let P1, P2 be non empty strict AlgebraStr over L; ( ( 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 )
; P1 = P2
then A27:
the carrier of P1 = the carrier of P2
by TARSKI:2;
then A28:
the lmult of P1 = the lmult of P2
by A27, BINOP_1:2;
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; verum