set f = J --> {};

A1: for i being set st i in J holds

(J --> {}) . i in F . i

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

hence ex b_{1} being Function of J,Sigma st

for i being set st i in J holds

b_{1} . i in F . i
by A1; :: thesis: verum

A1: for i being set st i in J holds

(J --> {}) . i in F . i

proof

A3:
dom (J --> {}) = J
by FUNCOP_1:13;
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;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

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

proof

then
J --> {} is Function of J,Sigma
by A3, FUNCT_2:2;
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;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

hence ex b

for i being set st i in J holds

b