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;

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

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

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;

A12: 1. P1 = 1. B by Def3
.= 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)

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;

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