let P1, P2 be non empty strict AlgebraStr over 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
A16: for x being set holds
( x in the carrier of P1 iff x is sequence of L ) and
A17: 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
A18: 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
A19: 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
A20: ( 0. P1 = 0_. L & 1. P1 = 1_. L ) and
A21: for x being set holds
( x in the carrier of P2 iff x is sequence of L ) and
A22: 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
A23: 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
A24: 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
A25: ( 0. P2 = 0_. L & 1. P2 = 1_. L ) ; :: thesis: P1 = P2
A26: now :: thesis: for x being object holds
( x in the carrier of P1 iff x in the carrier of P2 )
let x be object ; :: 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 A16;
hence ( x in the carrier of P1 iff x in the carrier of P2 ) by A21; :: thesis: verum
end;
then A27: the carrier of P1 = the carrier of P2 by TARSKI:2;
now :: thesis: for a being Element of L
for x being Element of P1 holds the lmult of P1 . (a,x) = the lmult of P2 . (a,x)
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 p = x as sequence of L by A16;
reconsider x1 = x as Element of P2 by A26;
reconsider a1 = a as Element of L ;
thus the lmult of P1 . (a,x) = a * x
.= a1 * p by A19
.= a1 * x1 by A24
.= the lmult of P2 . (a,x) ; :: thesis: verum
end;
then A28: the lmult of P1 = the lmult of P2 by ;
A29: now :: thesis: for x being Element of P1
for y being Element of P2 holds the multF of P1 . (x,y) = the multF of P2 . (x,y)
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 y1 = y as Element of P1 by A26;
reconsider x1 = x as Element of P2 by A26;
reconsider p = x as sequence of L by A16;
reconsider q = y as sequence of L by A21;
thus the multF of P1 . (x,y) = x * y1
.= p *' q by A18
.= x1 * y by A23
.= the multF of P2 . (x,y) ; :: thesis: verum
end;
now :: thesis: for x being Element of P1
for y being Element of P2 holds the addF of P1 . (x,y) = the addF of P2 . (x,y)
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 y1 = y as Element of P1 by A26;
reconsider x1 = x as Element of P2 by A26;
reconsider p = x as sequence of L by A16;
reconsider q = y as sequence of L by A21;
thus the addF of P1 . (x,y) = x + y1
.= p + q by A17
.= x1 + y by A22
.= the addF of P2 . (x,y) ; :: thesis: verum
end;
then the addF of P1 = the addF of P2 by ;
hence P1 = P2 by ; :: thesis: verum