let w1, w2 be BinOp of (n -tuples_on the carrier of R); :: thesis: ( ( for u, v being Tuple of n, the carrier of R holds w1 . (u,v) = u + v ) & ( for u, v being Tuple of n, the carrier of R holds w2 . (u,v) = u + v ) implies w1 = w2 )
assume that
A1: for u, v being Tuple of n, the carrier of R holds w1 . (u,v) = u + v and
A2: for u, v being Tuple of n, the carrier of R holds w2 . (u,v) = u + v ; :: thesis: w1 = w2

now :: thesis: for o being object st o in [:(n -tuples_on the carrier of R),(n -tuples_on the carrier of R):] holds
w1 . o = w2 . o

let o be object ; :: thesis: ( o in [:(n -tuples_on the carrier of R),(n -tuples_on the carrier of R):] implies w1 . o = w2 . o )
assume o in [:(n -tuples_on the carrier of R),(n -tuples_on the carrier of R):] ; :: thesis: w1 . o = w2 . o
then consider u, v being object such that
A3: ( u in n -tuples_on the carrier of R & v in n -tuples_on the carrier of R & o = [u,v] ) by ZFMISC_1:def 2;
reconsider u = u, v = v as Tuple of n, the carrier of R by A3, FINSEQ_2:131;
w1 . (u,v) = u + v by A1
.= w2 . (u,v) by A2 ;
hence w1 . o = w2 . o by A3; :: thesis: verum

end;

hence w1 = w2 by FUNCT_2:12; :: thesis: verum