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 Series of n,L ) ) & ( for x, y being Element of P1
for p, q being Series of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P1
for p, q being Series of n,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 Series of n,L st x = p holds
a * x = a * p ) & 0. P1 = 0_ (n,L) & 1. P1 = 1_ (n,L) & ( for x being set holds
( x in the carrier of P2 iff x is Series of n,L ) ) & ( for x, y being Element of P2
for p, q being Series of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P2
for p, q being Series of n,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 Series of n,L st x = p holds
a * x = a * p ) & 0. P2 = 0_ (n,L) & 1. P2 = 1_ (n,L) implies P1 = P2 )
assume that
A16: for x being set holds
( x in the carrier of P1 iff x is Series of n,L ) and
A17: for x, y being Element of P1
for p, q being Series of n,L st x = p & y = q holds
x + y = p + q and
A18: for x, y being Element of P1
for p, q being Series of n,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 Series of n,L st x = p holds
a * x = a * p and
A20: ( 0. P1 = 0_ (n,L) & 1. P1 = 1_ (n,L) ) and
A21: for x being set holds
( x in the carrier of P2 iff x is Series of n,L ) and
A22: for x, y being Element of P2
for p, q being Series of n,L st x = p & y = q holds
x + y = p + q and
A23: for x, y being Element of P2
for p, q being Series of n,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 Series of n,L st x = p holds
a * x = a * p and
A25: ( 0. P2 = 0_ (n,L) & 1. P2 = 1_ (n,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 Series of n,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 Series of n,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 A27, BINOP_1:2;

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 Series of n,L by A16;
reconsider q = y as Series of n,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 Series of n,L by A16;
reconsider q = y as Series of n,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 A27, BINOP_1:2;
hence P1 = P2 by A20, A25, A27, A29, A28, BINOP_1:2; :: thesis: verum