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 A7: 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 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
g2 . a,z = [(the Mult of X . [a,x]),(the Mult of Y . [a,y])] ; :: thesis: g1 = g2
for a being 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 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 set such that
A9: x in the carrier of X and
A10: y in the carrier of Y and
A11: z = [x,y] by ZFMISC_1:def 2;
reconsider y = y as VECTOR of Y by A10;
reconsider x = x as VECTOR of X by A9;
g1 . a,z = [(the Mult of X . [a,x]),(the Mult of Y . [a,y])] by A7, A11;
hence g1 . a,z = g2 . a,z by A8, A11; :: thesis: verum

end;

hence g1 = g2 by BINOP_1:2; :: thesis: verum