A1: 0_. L in { x where x is sequence of L : verum } ;
then reconsider Ca = { x where x is sequence of L : verum } as non empty set ;
defpred S₁[ set , set , set ] means ex p, q being sequence of L st
( p = $1 & q = $2 & $3 = p + q );
A2: for x, y being Element of Ca ex u being Element of Ca st S₁[x,y,u]

proof

let x, y be Element of Ca; :: thesis: ex u being Element of Ca st S₁[x,y,u]
x in Ca ;
then consider p being sequence of L such that
A3: x = p ;
y in Ca ;
then consider q being sequence of L such that
A4: y = q ;
p + q in Ca ;
then reconsider u = p + q as Element of Ca ;
take u ; :: thesis: S₁[x,y,u]
take p ; :: thesis: ex q being sequence of L st
( p = x & q = y & u = p + q )
take q ; :: thesis: ( p = x & q = y & u = p + q )
thus ( p = x & q = y & u = p + q ) by A3, A4; :: thesis: verum

end;

consider Ad being Function of [:Ca,Ca:],Ca such that
A5: for x, y being Element of Ca holds S₁[x,y,Ad . x,y] from BINOP_1:sch 3(A2);
defpred S₂[ set , set , set ] means ex p, q being sequence of L st
( p = $1 & q = $2 & $3 = p *' q );
A6: for x, y being Element of Ca ex u being Element of Ca st S₂[x,y,u]

proof

let x, y be Element of Ca; :: thesis: ex u being Element of Ca st S₂[x,y,u]
x in Ca ;
then consider p being sequence of L such that
A7: x = p ;
y in Ca ;
then consider q being sequence of L such that
A8: y = q ;
p *' q in Ca ;
then reconsider u = p *' q as Element of Ca ;
take u ; :: thesis: S₂[x,y,u]
take p ; :: thesis: ex q being sequence of L st
( p = x & q = y & u = p *' q )
take q ; :: thesis: ( p = x & q = y & u = p *' q )
thus ( p = x & q = y & u = p *' q ) by A7, A8; :: thesis: verum

end;

consider Mu being Function of [:Ca,Ca:],Ca such that
A9: for x, y being Element of Ca holds S₂[x,y,Mu . x,y] from BINOP_1:sch 3(A6);
1_. L in { x where x is sequence of L : verum } ;
then reconsider Un = 1_. L as Element of Ca ;
reconsider Ze = 0_. L as Element of Ca by A1;
defpred S₃[ Element of L, set , set ] means ex p being sequence of L st
( p = $2 & $3 = $1 * p );
A10: for a being Element of L
for x being Element of Ca ex u being Element of Ca st S₃[a,x,u]

proof

let a be Element of L; :: thesis: for x being Element of Ca ex u being Element of Ca st S₃[a,x,u]
let x be Element of Ca; :: thesis: ex u being Element of Ca st S₃[a,x,u]
x in Ca ;
then consider q being sequence of L such that
A11: x = q ;
a * q in Ca ;
then reconsider u = a * q as Element of Ca ;
take u ; :: thesis: S₃[a,x,u]
take q ; :: thesis: ( q = x & u = a * q )
thus ( q = x & u = a * q ) by A11; :: thesis: verum

end;

consider lm being Function of [:the carrier of L,Ca:],Ca such that
A12: for a being Element of L
for x being Element of Ca holds S₃[a,x,lm . a,x] from BINOP_1:sch 3(A10);
reconsider P = AlgebraStr(# Ca,Ad,Mu,Ze,Un,lm #) as non empty strict AlgebraStr of L ;
take P ; :: thesis: ( ( for x being set holds
( x in the carrier of P iff x is sequence of L ) ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P = 0_. L & 1. P = 1_. L )
thus for x being set holds
( x in the carrier of P iff x is sequence of L ) :: thesis: ( ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P = 0_. L & 1. P = 1_. L )

proof

let x be set ; :: thesis: ( x in the carrier of P iff x is sequence of L )
thus ( x in the carrier of P implies x is sequence of L ) :: thesis: ( x is sequence of L implies x in the carrier of P )

proof

assume x in the carrier of P ; :: thesis: x is sequence of L
then consider p being sequence of L such that
A13: x = p ;
thus x is sequence of L by A13; :: thesis: verum

end;

thus ( x is sequence of L implies x in the carrier of P ) ; :: thesis: verum

end;

thus for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q :: thesis: ( ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P = 0_. L & 1. P = 1_. L )

proof

let x, y be Element of P; :: thesis: for p, q being sequence of L st x = p & y = q holds
x + y = p + q
let p, q be sequence of L; :: thesis: ( x = p & y = q implies x + y = p + q )
assume that
A14: x = p and
A15: y = q ; :: thesis: x + y = p + q
consider p1, q1 being sequence of L such that
A16: p1 = x and
A17: q1 = y and
A18: Ad . x,y = p1 + q1 by A5;
thus x + y = p + q by A14, A15, A16, A17, A18; :: thesis: verum

end;

thus for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q :: thesis: ( ( for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P = 0_. L & 1. P = 1_. L )

proof

let x, y be Element of P; :: thesis: for p, q being sequence of L st x = p & y = q holds
x * y = p *' q
let p, q be sequence of L; :: thesis: ( x = p & y = q implies x * y = p *' q )
assume that
A19: x = p and
A20: y = q ; :: thesis: x * y = p *' q
consider p1, q1 being sequence of L such that
A21: p1 = x and
A22: q1 = y and
A23: Mu . x,y = p1 *' q1 by A9;
thus x * y = p *' q by A19, A20, A21, A22, A23; :: thesis: verum

end;

thus for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p :: thesis: ( 0. P = 0_. L & 1. P = 1_. L )

proof

let a be Element of L; :: thesis: for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p
let x be Element of P; :: thesis: for p being sequence of L st x = p holds
a * x = a * p
let p be sequence of L; :: thesis: ( x = p implies a * x = a * p )
assume A24: x = p ; :: thesis: a * x = a * p
consider p1 being sequence of L such that
A25: x = p1 and
A26: lm . a,x = a * p1 by A12;
thus a * x = a * p by A24, A25, A26; :: thesis: verum

end;

thus 0. P = 0_. L ; :: thesis: 1. P = 1_. L
thus 1. P = 1_. L ; :: thesis: verum