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)

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

hence
g1 = g2
; :: thesis: verum
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;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