let X1, X2 be Subset of Sigma; :: thesis: ( ( 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) ) ; :: thesis: ( 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) ) ; :: thesis: X1 = X2

now :: thesis: for a being Element of Sigma holds
( a in X1 iff a in X2 )

let a be Element of Sigma; :: thesis: ( 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; :: thesis: verum

end;

hence X1 = X2 by SUBSET_1:3; :: thesis: verum