set KK = the carrier of K;
defpred S₁[ set , set , set ] means for p1, p2 being Element of the carrier of K * st $1 = p1 & $2 = p2 holds
$3 = p1 + p2;
A1: for x, y being Element of the carrier of K * ex z being Element of the carrier of K * st S₁[x,y,z]

proof

let x, y be Element of the carrier of K * ; :: thesis: ex z being Element of the carrier of K * st S₁[x,y,z]
reconsider p1 = x, p2 = y as FinSequence of the carrier of K ;
reconsider pp = p1 + p2 as Element of the carrier of K * by FINSEQ_1:def 11;
take pp ; :: thesis: S₁[x,y,pp]
thus S₁[x,y,pp] ; :: thesis: verum

end;

consider A being Function of [:( the carrier of K *),( the carrier of K *):],( the carrier of K *) such that
A2: for x, y being Element of the carrier of K * holds S₁[x,y,A . (x,y)] from BINOP_1:sch 3(A1);
take A ; :: thesis: for p1, p2 being Element of the carrier of K * holds A . (p1,p2) = p1 + p2
thus for p1, p2 being Element of the carrier of K * holds A . (p1,p2) = p1 + p2 by A2; :: thesis: verum