set X = the carrier of V;
set Y = the carrier of W;
set Z = the carrier of K;
deffunc H₁( Element of the carrier of V, Element of the carrier of W) -> Element of the carrier of K = (f . $1,$2) + (g . $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₁(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) + (g . v,w)
thus for v being Vector of V
for w being Vector of W holds ff . v,w = (f . v,w) + (g . v,w) by A1; :: thesis: verum