set F = I --> Sigma;
A1: rng (I --> Sigma) c= bool Sigma
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (I --> Sigma) or y in bool Sigma )
assume y in rng (I --> Sigma) ; :: thesis: y in bool Sigma
then ex x being object st
( x in dom (I --> Sigma) & y = (I --> Sigma) . x ) by FUNCT_1:def 3;
then y = Sigma by FUNCOP_1:7;
hence y in bool Sigma by ZFMISC_1:def 1; :: thesis: verum
end;
A2: for i being set st i in I holds
(I --> Sigma) . i is SigmaField of Omega by FUNCOP_1:7;
dom (I --> Sigma) = I by FUNCOP_1:13;
then I --> Sigma is Function of I,(bool Sigma) by A1, FUNCT_2:2;
hence ex b1 being Function of I,(bool Sigma) st
for i being set st i in I holds
b1 . i is SigmaField of Omega by A2; :: thesis: verum