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 A4: 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 A5: 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 set such that
A6: ( x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1] ) by ZFMISC_1:def 2;
consider x2, y2 being set such that
A7: ( x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as VECTOR of X by A6, A7;
reconsider y1 = y1, y2 = y2 as VECTOR of Y by A6, A7;
( A1 . z1,z2 = [(the addF of X . [x1,x2]),(the addF of Y . [y1,y2])] & A2 . z1,z2 = [(the addF of X . [x1,x2]),(the addF of Y . [y1,y2])] ) by A4, A5, A6, A7;
hence A1 . z1,z2 = A2 . z1,z2 ; :: thesis: verum

end;

hence A1 = A2 by BINOP_1:2; :: thesis: verum