defpred S₁[ object , object , object ] means ex w, u, v being Element of n -tuples_on the carrier of R st
( w = $3 & u = $1 & v = $2 & w = u + v );
A0: for x, y being object st x in n -tuples_on the carrier of R & y in n -tuples_on the carrier of R holds
ex z being object st
( z in n -tuples_on the carrier of R & S₁[x,y,z] )

proof

let x, y be object ; :: thesis: ( x in n -tuples_on the carrier of R & y in n -tuples_on the carrier of R implies ex z being object st
( z in n -tuples_on the carrier of R & S₁[x,y,z] ) )
assume ( x in n -tuples_on the carrier of R & y in n -tuples_on the carrier of R ) ; :: thesis: ex z being object st
( z in n -tuples_on the carrier of R & S₁[x,y,z] )
then reconsider u = x, v = y as Tuple of n, the carrier of R by FINSEQ_2:131;
take z = u + v; :: thesis: ( z in n -tuples_on the carrier of R & S₁[x,y,z] )
thus z in n -tuples_on the carrier of R by FINSEQ_2:131; :: thesis: S₁[x,y,z]
ex w1, u1, v1 being Element of n -tuples_on the carrier of R st
( w1 = z & u1 = x & v1 = y & w1 = u1 + v1 )

proof

reconsider w = z, u = u, v = v as Element of n -tuples_on the carrier of R by FINSEQ_2:131;
take w ; :: thesis: ex u1, v1 being Element of n -tuples_on the carrier of R st
( w = z & u1 = x & v1 = y & w = u1 + v1 )
take u ; :: thesis: ex v1 being Element of n -tuples_on the carrier of R st
( w = z & u = x & v1 = y & w = u + v1 )
take v ; :: thesis: ( w = z & u = x & v = y & w = u + v )
thus ( w = z & u = x & v = y & w = u + v ) ; :: thesis: verum

end;

hence S₁[x,y,z] ; :: thesis: verum

end;

consider f being Function of [:(n -tuples_on the carrier of R),(n -tuples_on the carrier of R):],(n -tuples_on the carrier of R) such that
A1: for x, y being object st x in n -tuples_on the carrier of R & y in n -tuples_on the carrier of R holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(A0);
take f ; :: thesis: for u, v being Tuple of n, the carrier of R holds f . (u,v) = u + v

now :: thesis: for u, v being Tuple of n, the carrier of R holds f . (u,v) = u + v

let u, v be Tuple of n, the carrier of R; :: thesis: f . (u,v) = u + v
( u in n -tuples_on the carrier of R & v in n -tuples_on the carrier of R ) by FINSEQ_2:131;
then S₁[u,v,f . (u,v)] by A1;
hence f . (u,v) = u + v ; :: thesis: verum

end;

hence for u, v being Tuple of n, the carrier of R holds f . (u,v) = u + v ; :: thesis: verum