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

( 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 )

hence
X1 = X2
by SUBSET_1:3; :: thesis: verum( 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;( 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