set f = J --> {} ;
A0: dom (J --> {} ) = J by FUNCOP_1:19;
A2: 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 B0: 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:42;
hence (J --> {} ) . i in F . i by B0, FUNCOP_1:13; :: thesis: verum

end;

rng (J --> {} ) c= Sigma

proof

let y be set ; :: 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 set such that
B0: ( i in J & y = (J --> {} ) . i ) by A0, FUNCT_1:def 5;
B1: y in F . i by B0, A2;
F . i in bool Sigma by B0, FUNCT_2:7;
hence y in Sigma by B1; :: thesis: verum

end;

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