defpred S₁[ Element of the_set_of_RealSequences , Element of the_set_of_RealSequences , Element of the_set_of_RealSequences ] means $3 = (seq_id $1) + (seq_id $2);
A1: for x, y being Element of the_set_of_RealSequences ex z being Element of the_set_of_RealSequences st S₁[x,y,z]

proof

let x, y be Element of the_set_of_RealSequences ; :: thesis: ex z being Element of the_set_of_RealSequences st S₁[x,y,z]
(seq_id x) + (seq_id y) is Element of the_set_of_RealSequences by Def1;
hence ex z being Element of the_set_of_RealSequences st S₁[x,y,z] ; :: thesis: verum

end;

ex ADD being BinOp of the_set_of_RealSequences st
for a, b being Element of the_set_of_RealSequences holds S₁[a,b,ADD . (a,b)] from BINOP_1:sch 3(A1);
then consider ADD being BinOp of the_set_of_RealSequences such that
A2: for a, b being Element of the_set_of_RealSequences holds ADD . (a,b) = (seq_id a) + (seq_id b) ;
thus ex b₁ being BinOp of the_set_of_RealSequences st
for a, b being Element of the_set_of_RealSequences holds b₁ . (a,b) = (seq_id a) + (seq_id b) by A2; :: thesis: verum