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₁( 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₁(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