reconsider aa = a as Element of INT.Ring ;
set X = the carrier of V;
set Y = the carrier of W;
deffunc H1( Element of the carrier of V, Element of the carrier of W) -> Element of the carrier of INT.Ring = In ((aa * (f . ($1,$2))), the carrier of INT.Ring);
consider ff being Function of [: the carrier of V, the carrier of W:],INT.Ring such that
A1:
for x being Element of the carrier of V
for y being Element of the carrier of W holds ff . (x,y) = H1(x,y)
from BINOP_1:sch 4();
reconsider ff = ff as Form of V,W ;
take
ff
; for v being Vector of V
for w being Vector of W holds ff . (v,w) = a * (f . (v,w))
let v be Vector of V; for w being Vector of W holds ff . (v,w) = a * (f . (v,w))
let w be Vector of W; ff . (v,w) = a * (f . (v,w))
ff . (v,w) = H1(v,w)
by A1;
then
ff . (v,w) = a * (f . (v,w))
;
hence
ff . (v,w) = a * (f . (v,w))
; verum