let P1, P2 be non empty strict AlgebraStr of L; :: thesis: ( ( for x being set holds
( x in the carrier of P1 iff x is sequence of L ) ) & ( for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P1
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 P1
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P1 = 0_. L & 1. P1 = 1_. L & ( for x being set holds
( x in the carrier of P2 iff x is sequence of L ) ) & ( for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P2
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 P2
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P2 = 0_. L & 1. P2 = 1_. L implies P1 = P2 )
assume that
A27: for x being set holds
( x in the carrier of P1 iff x is sequence of L ) and
A28: for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q and
A29: for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q and
A30: for a being Element of L
for x being Element of P1
for p being sequence of L st x = p holds
a * x = a * p and
A31: 0. P1 = 0_. L and
A32: 1. P1 = 1_. L and
A33: for x being set holds
( x in the carrier of P2 iff x is sequence of L ) and
A34: for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q and
A35: for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q and
A36: for a being Element of L
for x being Element of P2
for p being sequence of L st x = p holds
a * x = a * p and
A37: 0. P2 = 0_. L and
A38: 1. P2 = 1_. L ; :: thesis: P1 = P2

A39: now

let x be set ; :: thesis: ( x in the carrier of P1 iff x in the carrier of P2 )
( x in the carrier of P1 iff x is sequence of L ) by A27;
hence ( x in the carrier of P1 iff x in the carrier of P2 ) by A33; :: thesis: verum

end;

then A40: the carrier of P1 = the carrier of P2 by TARSKI:2;

now

let x be Element of P1; :: thesis: for y being Element of P2 holds the addF of P1 . x,y = the addF of P2 . x,y
let y be Element of P2; :: thesis: the addF of P1 . x,y = the addF of P2 . x,y
reconsider x1 = x as Element of P2 by A39;
reconsider y1 = y as Element of P1 by A39;
reconsider p = x as sequence of L by A27;
reconsider q = y as sequence of L by A33;
thus the addF of P1 . x,y = x + y1
.= p + q by A28
.= x1 + y by A34
.= the addF of P2 . x,y ; :: thesis: verum

end;

then A41: the addF of P1 = the addF of P2 by A40, BINOP_1:2;

A42: now

let x be Element of P1; :: thesis: for y being Element of P2 holds the multF of P1 . x,y = the multF of P2 . x,y
let y be Element of P2; :: thesis: the multF of P1 . x,y = the multF of P2 . x,y
reconsider x1 = x as Element of P2 by A39;
reconsider y1 = y as Element of P1 by A39;
reconsider p = x as sequence of L by A27;
reconsider q = y as sequence of L by A33;
thus the multF of P1 . x,y = x * y1
.= p *' q by A29
.= x1 * y by A35
.= the multF of P2 . x,y ; :: thesis: verum

end;

now

let a be Element of L; :: thesis: for x being Element of P1 holds the lmult of P1 . a,x = the lmult of P2 . a,x
let x be Element of P1; :: thesis: the lmult of P1 . a,x = the lmult of P2 . a,x
reconsider a1 = a as Element of L ;
reconsider x1 = x as Element of P2 by A39;
reconsider p = x as sequence of L by A27;
thus the lmult of P1 . a,x = a * x
.= a1 * p by A30
.= a1 * x1 by A36
.= the lmult of P2 . a,x ; :: thesis: verum

end;

then the lmult of P1 = the lmult of P2 by A40, BINOP_1:2;
hence P1 = P2 by A31, A32, A37, A38, A40, A41, A42, BINOP_1:2; :: thesis: verum