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 = (f . ($1,$2)) + (g . ($1,$2));
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) = (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