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 A4: 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 A5: 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
A6: ( x in the carrier of X & y in the carrier of Y & z = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x as VECTOR of X by A6;
reconsider y = y as VECTOR of Y by A6;
( g1 . a,z = [(the Mult of X . [a,x]),(the Mult of Y . [a,y])] & g2 . a,z = [(the Mult of X . [a,x]),(the Mult of Y . [a,y])] ) by A4, A5, A6;
hence g1 . a,z = g2 . a,z ; :: thesis: verum

end;

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