set C = Carrier f;
defpred S₁[ object , object , object ] means ex i being Element of NAT ex x, y being Element of (f . i) st
( x = $1 & y = $2 & $3 = x + y );
A: for a, b being Element of Carrier f ex z being Element of Carrier f st S₁[a,b,z]

proof

let a, b be Element of Carrier f; :: thesis: ex z being Element of Carrier f st S₁[a,b,z]
consider Y being set such that
A0: ( a in Y & Y in { the carrier of (f . i) where i is Element of NAT : verum } ) by TARSKI:def 4;
consider i being Element of NAT such that
A1: Y = the carrier of (f . i) by A0;
consider Z being set such that
A2: ( b in Z & Z in { the carrier of (f . i) where i is Element of NAT : verum } ) by TARSKI:def 4;
consider j being Element of NAT such that
A3: Z = the carrier of (f . j) by A2;

per cases ( i <= j or j <= i ) ;

suppose i <= j ; :: thesis: ex z being Element of Carrier f st S₁[a,b,z]

then reconsider x = a, y = b as Element of (f . j) by A0, A1, A2, A3, lem1;
( x + y in the carrier of (f . j) & the carrier of (f . j) in { the carrier of (f . n) where n is Element of NAT : verum } ) ;
then reconsider z = x + y as Element of Carrier f by TARSKI:def 4;
take z ; :: thesis: S₁[a,b,z]
thus S₁[a,b,z] ; :: thesis: verum

end;

suppose j <= i ; :: thesis: ex z being Element of Carrier f st S₁[a,b,z]

then reconsider x = a, y = b as Element of (f . i) by A0, A1, A2, A3, lem1;
( x + y in the carrier of (f . i) & the carrier of (f . i) in { the carrier of (f . n) where n is Element of NAT : verum } ) ;
then reconsider z = x + y as Element of Carrier f by TARSKI:def 4;
take z ; :: thesis: S₁[a,b,z]
thus S₁[a,b,z] ; :: thesis: verum

end;

end;

end;

consider A being Function of [:(Carrier f),(Carrier f):],(Carrier f) such that
B: for x, y being Element of Carrier f holds S₁[x,y,A . (x,y)] from BINOP_1:sch 3(A);
reconsider A = A as BinOp of (Carrier f) ;
take A ; :: thesis: for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & A . (a,b) = x + y )
thus for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & A . (a,b) = x + y ) by B; :: thesis: verum