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

proof

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

end;

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