reconsider aa = a as Element of INT.Ring ;
set X = the carrier of V;
set Y = the carrier of W;
deffunc H₁( 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) = H₁(x,y) from BINOP_1:sch 4();
reconsider ff = ff as Form of V,W ;
take ff ; :: thesis: 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; :: thesis: for w being Vector of W holds ff . (v,w) = a * (f . (v,w))
let w be Vector of W; :: thesis: ff . (v,w) = a * (f . (v,w))
ff . (v,w) = H₁(v,w) by A1;
then ff . (v,w) = a * (f . (v,w)) ;
hence ff . (v,w) = a * (f . (v,w)) ; :: thesis: verum