set F = I --> Sigma;
A0: dom (I --> Sigma) = I by FUNCOP_1:19;
rng (I --> Sigma) c= bool Sigma

proof

let y be set ; :: 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 set st
( x in dom (I --> Sigma) & y = (I --> Sigma) . x ) by FUNCT_1:def 5;
then y = Sigma by FUNCOP_1:13;
hence y in bool Sigma by ZFMISC_1:def 1; :: thesis: verum

end;

then A2: I --> Sigma is Function of I,(bool Sigma) by A0, FUNCT_2:4;
for i being set st i in I holds
(I --> Sigma) . i is SigmaField of Omega by FUNCOP_1:13;
hence ex b₁ being Function of I,(bool Sigma) st
for i being set st i in I holds
b₁ . i is SigmaField of Omega by A2; :: thesis: verum