defpred S₁[ set ] means for b being Element of B holds P . ($1 /\ b) = (P . $1) * (P . b);
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Sigma & S₁[x] ) ) from XFAMILY:sch 1();
for x being object st x in X holds
x in Sigma by A1;
then reconsider X = X as Subset of Sigma by TARSKI:def 3;
take X ; :: thesis: for a being Element of Sigma holds
( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )
let a be Element of Sigma; :: thesis: ( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )
thus ( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) by A1; :: thesis: verum