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 ;

reconsider Ze = 0_. L as Element of Ca by A1;

defpred S_{1}[ 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_{1}[x,y,u]

A5: for x, y being Element of Ca holds S_{1}[x,y,Ad . (x,y)]
from BINOP_1:sch 3(A2);

1_. L in { x where x is sequence of L : verum } ;

then reconsider Un = 1_. L as Element of Ca ;

defpred S_{2}[ 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_{2}[x,y,u]

A9: for x, y being Element of Ca holds S_{2}[x,y,Mu . (x,y)]
from BINOP_1:sch 3(A6);

defpred S_{3}[ 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_{3}[a,x,u]

A12: for a being Element of L

for x being Element of Ca holds S_{3}[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 over 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 )

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 )

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 )

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 )

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

then reconsider Ca = { x where x is sequence of L : verum } as non empty set ;

reconsider Ze = 0_. L as Element of Ca by A1;

defpred S

( p = $1 & q = $2 & $3 = p + q );

A2: for x, y being Element of Ca ex u being Element of Ca st S

proof

consider Ad being Function of [:Ca,Ca:],Ca such that
let x, y be Element of Ca; :: thesis: ex u being Element of Ca st S_{1}[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_{1}[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;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

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

A5: for x, y being Element of Ca holds S

1_. L in { x where x is sequence of L : verum } ;

then reconsider Un = 1_. L as Element of Ca ;

defpred S

( p = $1 & q = $2 & $3 = p *' q );

A6: for x, y being Element of Ca ex u being Element of Ca st S

proof

consider Mu being Function of [:Ca,Ca:],Ca such that
let x, y be Element of Ca; :: thesis: ex u being Element of Ca st S_{2}[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_{2}[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;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

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

A9: for x, y being Element of Ca holds S

defpred S

( 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

proof

consider lm being Function of [: the carrier of L,Ca:],Ca such that
let a be Element of L; :: thesis: for x being Element of Ca ex u being Element of Ca st S_{3}[a,x,u]

let x be Element of Ca; :: thesis: ex u being Element of Ca st S_{3}[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_{3}[a,x,u]

take q ; :: thesis: ( q = x & u = a * q )

thus ( q = x & u = a * q ) by A11; :: thesis: verum

end;let x be Element of Ca; :: thesis: ex u being Element of Ca st S

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

take q ; :: thesis: ( q = x & u = a * q )

thus ( q = x & u = a * q ) by A11; :: thesis: verum

A12: for a being Element of L

for x being Element of Ca holds S

reconsider P = AlgebraStr(# Ca,Ad,Mu,Ze,Un,lm #) as non empty strict AlgebraStr over 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

thus
for x, y being Element of P
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 )

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

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

then ex p being sequence of L st x = p ;

hence x is sequence of L ; :: thesis: verum

end;then ex p being sequence of L st x = p ;

hence x is sequence of L ; :: thesis: verum

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

thus
for x, y being Element of P
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 A13: ( x = p & y = q ) ; :: thesis: x + y = p + q

ex p1, q1 being sequence of L st

( p1 = x & q1 = y & Ad . (x,y) = p1 + q1 ) by A5;

hence x + y = p + q by A13; :: thesis: verum

end;x + y = p + q

let p, q be sequence of L; :: thesis: ( x = p & y = q implies x + y = p + q )

assume A13: ( x = p & y = q ) ; :: thesis: x + y = p + q

ex p1, q1 being sequence of L st

( p1 = x & q1 = y & Ad . (x,y) = p1 + q1 ) by A5;

hence x + y = p + q by A13; :: thesis: verum

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

thus
for a being Element of L
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 A14: ( x = p & y = q ) ; :: thesis: x * y = p *' q

ex p1, q1 being sequence of L st

( p1 = x & q1 = y & Mu . (x,y) = p1 *' q1 ) by A9;

hence x * y = p *' q by A14; :: thesis: verum

end;x * y = p *' q

let p, q be sequence of L; :: thesis: ( x = p & y = q implies x * y = p *' q )

assume A14: ( x = p & y = q ) ; :: thesis: x * y = p *' q

ex p1, q1 being sequence of L st

( p1 = x & q1 = y & Mu . (x,y) = p1 *' q1 ) by A9;

hence x * y = p *' q by A14; :: thesis: verum

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

thus
0. P = 0_. L
; :: thesis: 1. P = 1_. L
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 A15: x = p ; :: thesis: a * x = a * p

ex p1 being sequence of L st

( x = p1 & lm . (a,x) = a * p1 ) by A12;

hence a * x = a * p by A15; :: thesis: verum

end;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 A15: x = p ; :: thesis: a * x = a * p

ex p1 being sequence of L st

( x = p1 & lm . (a,x) = a * p1 ) by A12;

hence a * x = a * p by A15; :: thesis: verum

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