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)

proof

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;

hence A1 = A2 ; :: thesis: verum