let X1, X2 be Subset of Sigma; ( ( for a being Element of Sigma holds
( a in X1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) & ( for a being Element of Sigma holds
( a in X2 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) implies X1 = X2 )
assume A2:
for a being Element of Sigma holds
( a in X1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )
; ( ex a being Element of Sigma st
( ( a in X2 implies for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) implies ( ( for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) & not a in X2 ) ) or X1 = X2 )
assume A3:
for a being Element of Sigma holds
( a in X2 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )
; X1 = X2
now for a being Element of Sigma holds
( a in X1 iff a in X2 )let a be
Element of
Sigma;
( a in X1 iff a in X2 )
(
a in X1 iff for
b being
Element of
B holds
P . (a /\ b) = (P . a) * (P . b) )
by A2;
hence
(
a in X1 iff
a in X2 )
by A3;
verum end;
hence
X1 = X2
by SUBSET_1:3; verum