deffunc H₁( Vector of V, Vector of W) -> Element of the carrier of INT.Ring = (f . $1) * (g . $2);
set c1 = the carrier of V;
set c2 = the carrier of W;
consider i being Function of [: the carrier of V, the carrier of W:], the carrier of INT.Ring such that
A1: for x being Element of the carrier of V
for y being Element of the carrier of W holds i . (x,y) = H₁(x,y) from BINOP_1:sch 4();
reconsider i = i as Form of V,W ;
take i ; :: thesis: for v being Vector of V
for w being Vector of W holds i . (v,w) = (f . v) * (g . w)
thus for v being Vector of V
for w being Vector of W holds i . (v,w) = (f . v) * (g . w) by A1; :: thesis: verum