let g1, g2 be Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]; :: thesis: ( ( for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) & ( for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) implies g1 = g2 )
assume A8: for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ; :: thesis: ( ex a being Real ex z being Element of [: the carrier of X, the carrier of Y:] ex x being VECTOR of X ex y being VECTOR of Y st
( z = [x,y] & not g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) or g1 = g2 )
assume A9: for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ; :: thesis: g1 = g2
for a being Element of REAL
for z being Element of [: the carrier of X, the carrier of Y:] holds g1 . (a,z) = g2 . (a,z)

proof

let a be Element of REAL ; :: thesis: for z being Element of [: the carrier of X, the carrier of Y:] holds g1 . (a,z) = g2 . (a,z)
let z be Element of [: the carrier of X, the carrier of Y:]; :: thesis: g1 . (a,z) = g2 . (a,z)
consider x, y being object such that
A10: x in the carrier of X and
A11: y in the carrier of Y and
A12: z = [x,y] by ZFMISC_1:def 2;
reconsider y = y as VECTOR of Y by A11;
reconsider x = x as VECTOR of X by A10;
g1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] by A8, A12;
hence g1 . (a,z) = g2 . (a,z) by A9, A12; :: thesis: verum

end;

hence g1 = g2 ; :: thesis: verum