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

hence P1 = P2 by A20, A25, A27, A29, A28, BINOP_1:2; :: thesis: verum

( 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 )

then A27:
the carrier of P1 = the carrier of P2
by TARSKI:2;( 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;( 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

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)

then A28:
the lmult of P1 = the lmult of P2
by A27, BINOP_1:2;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;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

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)

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

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)

then
the addF of P1 = the addF of P2
by A27, BINOP_1:2;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;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

hence P1 = P2 by A20, A25, A27, A29, A28, BINOP_1:2; :: thesis: verum