set X = the carrier of V;
set Y = the carrier of W;
deffunc H1( 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) = H1(x,y)
from BINOP_1:sch 4();
reconsider ff = ff as Form of V,W ;
take
ff
; 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; verum