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) ;
A3: ADD is commutative

proof

now

let a, b be Element of the_set_of_ComplexSequences ; :: thesis: ADD . a,b = ADD . b,a
thus ADD . a,b = (seq_id a) + (seq_id b) by A2
.= ADD . b,a by A2 ; :: thesis: verum

end;

hence ADD is commutative by BINOP_1:def 2; :: thesis: verum

end;

ADD is associative

proof

now

let a, b, c be Element of the_set_of_ComplexSequences ; :: thesis: ADD . a,(ADD . b,c) = ADD . (ADD . a,b),c
A4: seq_id (ADD . b,c) = ADD . b,c by Def2
.= (seq_id b) + (seq_id c) by A2 ;
A5: (seq_id a) + (seq_id b) = ADD . a,b by A2
.= seq_id (ADD . a,b) by Def2 ;
thus ADD . a,(ADD . b,c) = (seq_id a) + (seq_id (ADD . b,c)) by A2
.= ((seq_id a) + (seq_id b)) + (seq_id c) by A4, COMSEQ_1:9
.= ADD . (ADD . a,b),c by A2, A5 ; :: thesis: verum

end;

hence ADD is associative by BINOP_1:def 3; :: thesis: verum

end;

hence ex ADD being BinOp of the_set_of_ComplexSequences st
( ( for a, b being Element of the_set_of_ComplexSequences holds ADD . a,b = (seq_id a) + (seq_id b) ) & ADD is commutative & ADD is associative ) by A2, A3; :: thesis: verum