let X be set ; :: thesis: for S being SigmaField of X
for N being Function of NAT,S
for A being Element of S ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
let S be SigmaField of X; :: thesis: for N being Function of NAT,S
for A being Element of S ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
let N be Function of NAT,S; :: thesis: for A being Element of S ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
let A be Element of S; :: thesis: ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
defpred S₁[ set , set ] means ( $1 in NAT implies $2 = A /\ (N . $1) );
A1: for x being set st x in NAT holds
ex y being set st
( y in S & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in S & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in S & S₁[x,y] )
then reconsider x = x as Element of NAT ;
consider y being set such that
A2: y = A /\ (N . x) ;
take y ; :: thesis: ( y in S & S₁[x,y] )
thus ( y in S & S₁[x,y] ) by A2; :: thesis: verum

end;

ex F being Function of NAT,S st
for x being set st x in NAT holds
S₁[x,F . x] from FUNCT_2:sch 1(A1);
then consider F being Function of NAT,S such that
A3: for x being set st x in NAT holds
S₁[x,F . x] ;
take F ; :: thesis: for n being Element of NAT holds F . n = A /\ (N . n)
thus for n being Element of NAT holds F . n = A /\ (N . n) by A3; :: thesis: verum