set X = the carrier of V;

set Y = the carrier of W;

set Z = the carrier of K;

deffunc H_{1}( Element of the carrier of V, Element of the carrier of W) -> Element of the carrier of K = a * (f . ($1,$2));

consider ff being Function of [: the carrier of V, the carrier of W:], the carrier of K 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_{1}(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))

thus for v being Vector of V

for w being Vector of W holds ff . (v,w) = a * (f . (v,w)) by A1; :: thesis: verum

set Y = the carrier of W;

set Z = the carrier of K;

deffunc H

consider ff being Function of [: the carrier of V, the carrier of W:], the carrier of K 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

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))

thus for v being Vector of V

for w being Vector of W holds ff . (v,w) = a * (f . (v,w)) by A1; :: thesis: verum