deffunc H_{1}( Vector of V, Vector of W) -> Element of the carrier of K = (f . $1) * (g . $2);

set c1 = the carrier of V;

set c2 = the carrier of W;

set k = the carrier of K;

consider i 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 i . (x,y) = H_{1}(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

set c1 = the carrier of V;

set c2 = the carrier of W;

set k = the carrier of K;

consider i 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 i . (x,y) = H

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