set f = J --> {};
A1: for i being set st i in J holds
(J --> {}) . i in F . i

proof

let i be set ; :: thesis: ( i in J implies (J --> {}) . i in F . i )
assume A2: i in J ; :: thesis: (J --> {}) . i in F . i
then F . i is SigmaField of Omega by Def2;
then {} in F . i by PROB_1:4;
hence (J --> {}) . i in F . i by A2, FUNCOP_1:7; :: thesis: verum

end;

A3: dom (J --> {}) = J by FUNCOP_1:13;
rng (J --> {}) c= Sigma

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (J --> {}) or y in Sigma )
assume y in rng (J --> {}) ; :: thesis: y in Sigma
then consider i being object such that
A4: ( i in J & y = (J --> {}) . i ) by A3, FUNCT_1:def 3;
( y in F . i & F . i in bool Sigma ) by A1, A4, FUNCT_2:5;
hence y in Sigma ; :: thesis: verum

end;

then J --> {} is Function of J,Sigma by A3, FUNCT_2:2;
hence ex b₁ being Function of J,Sigma st
for i being set st i in J holds
b₁ . i in F . i by A1; :: thesis: verum