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) ;

now

let a, b, c be Element of the_set_of_RealSequences ; :: thesis: ADD . (a,(ADD . (b,c))) = ADD . ((ADD . (a,b)),c)
A3: seq_id (ADD . (b,c)) = ADD . (b,c) by Def2
.= (seq_id b) + (seq_id c) by A2 ;
A4: (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 A3, SEQ_1:20
.= ADD . ((ADD . (a,b)),c) by A2, A4 ; :: thesis: verum

end;

then A5: ADD is associative by BINOP_1:def 3;

now

let a, b be Element of the_set_of_RealSequences ; :: 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;

then ADD is commutative by BINOP_1:def 2;
hence ex ADD being BinOp of the_set_of_RealSequences st
( ( for a, b being Element of the_set_of_RealSequences holds ADD . (a,b) = (seq_id a) + (seq_id b) ) & ADD is commutative & ADD is associative ) by A2, A5; :: thesis: verum