set F = I --> Sigma;

A1: rng (I --> Sigma) c= bool Sigma

(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 b_{1} being Function of I,(bool Sigma) st

for i being set st i in I holds

b_{1} . i is SigmaField of Omega
by A2; :: thesis: verum

A1: rng (I --> Sigma) c= bool Sigma

proof

A2:
for i being set st i in I holds
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;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

(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 b

for i being set st i in I holds

b