let P1, P2 be non empty strict Subalgebra of B; :: thesis: ( A c= the carrier of P1 & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of P1 c= the carrier of C ) & A c= the carrier of P2 & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of P2 c= the carrier of C ) implies P1 = P2 )

assume ( A c= the carrier of P1 & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of P1 c= the carrier of C ) & A c= the carrier of P2 & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of P2 c= the carrier of C ) ) ; :: thesis: P1 = P2

then A6: ( the carrier of P1 c= the carrier of P2 & the carrier of P2 c= the carrier of P1 ) ;

then A7: the carrier of P1 = the carrier of P2 by XBOOLE_0:def 10;

A10: 0. P1 = 0. B by Def3

.= 0. P2 by Def3 ;

.= 1. P2 by Def3 ;

hence P1 = P2 by A7, A9, A10, A12, A11, BINOP_1:2; :: thesis: verum

the carrier of P1 c= the carrier of C ) & A c= the carrier of P2 & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of P2 c= the carrier of C ) implies P1 = P2 )

assume ( A c= the carrier of P1 & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of P1 c= the carrier of C ) & A c= the carrier of P2 & ( for C being Subalgebra of B st A c= the carrier of C holds

the carrier of P2 c= the carrier of C ) ) ; :: thesis: P1 = P2

then A6: ( the carrier of P1 c= the carrier of P2 & the carrier of P2 c= the carrier of P1 ) ;

then A7: the carrier of P1 = the carrier of P2 by XBOOLE_0:def 10;

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)

then A9:
the multF of P1 = the multF of P2
by A7, BINOP_1:2;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 A6;

reconsider x1 = x as Element of P2 by A6;

A8: the carrier of P2 c= the carrier of B by Def3;

then reconsider x9 = x1 as Element of B ;

reconsider y9 = y as Element of B by A8;

thus the multF of P1 . (x,y) = x * y1

.= x9 * y9 by Th16

.= x1 * y by Th16

.= 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 A6;

reconsider x1 = x as Element of P2 by A6;

A8: the carrier of P2 c= the carrier of B by Def3;

then reconsider x9 = x1 as Element of B ;

reconsider y9 = y as Element of B by A8;

thus the multF of P1 . (x,y) = x * y1

.= x9 * y9 by Th16

.= x1 * y by Th16

.= the multF of P2 . (x,y) ; :: thesis: verum

A10: 0. P1 = 0. B by Def3

.= 0. P2 by Def3 ;

A11: now :: thesis: for x being Element of L

for y being Element of P1 holds the lmult of P1 . (x,y) = the lmult of P2 . (x,y)

A12: 1. P1 =
1. B
by Def3
for y being Element of P1 holds the lmult of P1 . (x,y) = the lmult of P2 . (x,y)

let x be Element of L; :: thesis: for y being Element of P1 holds the lmult of P1 . (x,y) = the lmult of P2 . (x,y)

let y be Element of P1; :: thesis: the lmult of P1 . (x,y) = the lmult of P2 . (x,y)

reconsider y1 = y as Element of P2 by A6;

the carrier of P2 c= the carrier of B by Def3;

then reconsider y9 = y1 as Element of B ;

thus the lmult of P1 . (x,y) = x * y

.= x * y9 by Th17

.= x * y1 by Th17

.= the lmult of P2 . (x,y) ; :: thesis: verum

end;let y be Element of P1; :: thesis: the lmult of P1 . (x,y) = the lmult of P2 . (x,y)

reconsider y1 = y as Element of P2 by A6;

the carrier of P2 c= the carrier of B by Def3;

then reconsider y9 = y1 as Element of B ;

thus the lmult of P1 . (x,y) = x * y

.= x * y9 by Th17

.= x * y1 by Th17

.= the lmult of P2 . (x,y) ; :: thesis: verum

.= 1. P2 by Def3 ;

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 A7, 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 A6;

reconsider x1 = x as Element of P2 by A6;

A13: the carrier of P2 c= the carrier of B by Def3;

then reconsider x9 = x1 as Element of B ;

reconsider y9 = y as Element of B by A13;

thus the addF of P1 . (x,y) = x + y1

.= x9 + y9 by Th15

.= x1 + y by Th15

.= 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 A6;

reconsider x1 = x as Element of P2 by A6;

A13: the carrier of P2 c= the carrier of B by Def3;

then reconsider x9 = x1 as Element of B ;

reconsider y9 = y as Element of B by A13;

thus the addF of P1 . (x,y) = x + y1

.= x9 + y9 by Th15

.= x1 + y by Th15

.= the addF of P2 . (x,y) ; :: thesis: verum

hence P1 = P2 by A7, A9, A10, A12, A11, BINOP_1:2; :: thesis: verum