let A1, A2 be BinOp of [: the carrier of X, the carrier of Y:]; :: thesis: ( ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:]

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

A1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) & ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:]

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) implies A1 = A2 )

assume A12: for z1, z2 being Element of [: the carrier of X, the carrier of Y:]

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

A1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ; :: thesis: ( ex z1, z2 being Element of [: the carrier of X, the carrier of Y:] ex x1, x2 being VECTOR of X ex y1, y2 being VECTOR of Y st

( z1 = [x1,y1] & z2 = [x2,y2] & not A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) or A1 = A2 )

assume A13: for z1, z2 being Element of [: the carrier of X, the carrier of Y:]

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ; :: thesis: A1 = A2

for z1, z2 being Element of [: the carrier of X, the carrier of Y:] holds A1 . (z1,z2) = A2 . (z1,z2)

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

A1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) & ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:]

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) implies A1 = A2 )

assume A12: for z1, z2 being Element of [: the carrier of X, the carrier of Y:]

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

A1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ; :: thesis: ( ex z1, z2 being Element of [: the carrier of X, the carrier of Y:] ex x1, x2 being VECTOR of X ex y1, y2 being VECTOR of Y st

( z1 = [x1,y1] & z2 = [x2,y2] & not A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) or A1 = A2 )

assume A13: for z1, z2 being Element of [: the carrier of X, the carrier of Y:]

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ; :: thesis: A1 = A2

for z1, z2 being Element of [: the carrier of X, the carrier of Y:] holds A1 . (z1,z2) = A2 . (z1,z2)

proof

hence
A1 = A2
; :: thesis: verum
let z1, z2 be Element of [: the carrier of X, the carrier of Y:]; :: thesis: A1 . (z1,z2) = A2 . (z1,z2)

consider x1, y1 being object such that

A14: x1 in the carrier of X and

A15: y1 in the carrier of Y and

A16: z1 = [x1,y1] by ZFMISC_1:def 2;

consider x2, y2 being object such that

A17: x2 in the carrier of X and

A18: y2 in the carrier of Y and

A19: z2 = [x2,y2] by ZFMISC_1:def 2;

reconsider y1 = y1, y2 = y2 as VECTOR of Y by A15, A18;

reconsider x1 = x1, x2 = x2 as VECTOR of X by A14, A17;

A1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] by A12, A16, A19;

hence A1 . (z1,z2) = A2 . (z1,z2) by A13, A16, A19; :: thesis: verum

end;consider x1, y1 being object such that

A14: x1 in the carrier of X and

A15: y1 in the carrier of Y and

A16: z1 = [x1,y1] by ZFMISC_1:def 2;

consider x2, y2 being object such that

A17: x2 in the carrier of X and

A18: y2 in the carrier of Y and

A19: z2 = [x2,y2] by ZFMISC_1:def 2;

reconsider y1 = y1, y2 = y2 as VECTOR of Y by A15, A18;

reconsider x1 = x1, x2 = x2 as VECTOR of X by A14, A17;

A1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] by A12, A16, A19;

hence A1 . (z1,z2) = A2 . (z1,z2) by A13, A16, A19; :: thesis: verum