set K = F_Complex ;

set X = the carrier of V;

set Y = the carrier of W;

set Z = the carrier of F_Complex;

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

consider ff being Function of [: the carrier of V, the carrier of W:], the carrier of F_Complex 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) = (f . (v,w)) *'

thus for v being Vector of V

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

set X = the carrier of V;

set Y = the carrier of W;

set Z = the carrier of F_Complex;

deffunc H

consider ff being Function of [: the carrier of V, the carrier of W:], the carrier of F_Complex 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) = (f . (v,w)) *'

thus for v being Vector of V

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