defpred S_{1}[ set , set ] means c_{2} is SigmaField of (S . S);

set X = union (rng S);

A1: for n being Element of NAT ex y being Element of bool (bool (union (rng S))) st S_{1}[n,y]

A2: for n being Element of NAT holds S_{1}[n,F . n]
from FUNCT_2:sch 3(A1);

take F ; :: thesis: F is S -SigmaField_sequence-like

let n be Nat; :: according to RANDOM_3:def 8 :: thesis: F . n is SigmaField of (S . n)

n in NAT by ORDINAL1:def 12;

hence F . n is SigmaField of (S . n) by A2; :: thesis: verum

set X = union (rng S);

A1: for n being Element of NAT ex y being Element of bool (bool (union (rng S))) st S

proof

consider F being Function of NAT,(bool (bool (union (rng S)))) such that
let n be Element of NAT ; :: thesis: ex y being Element of bool (bool (union (rng S))) st S_{1}[n,y]

set y = the SigmaField of (S . n);

dom S = NAT by PARTFUN1:def 2;

then S . n in rng S by FUNCT_1:3;

then bool (S . n) c= bool (union (rng S)) by ZFMISC_1:67, ZFMISC_1:74;

hence ex y being Element of bool (bool (union (rng S))) st S_{1}[n,y]
; :: thesis: verum

end;set y = the SigmaField of (S . n);

dom S = NAT by PARTFUN1:def 2;

then S . n in rng S by FUNCT_1:3;

then bool (S . n) c= bool (union (rng S)) by ZFMISC_1:67, ZFMISC_1:74;

hence ex y being Element of bool (bool (union (rng S))) st S

A2: for n being Element of NAT holds S

take F ; :: thesis: F is S -SigmaField_sequence-like

let n be Nat; :: according to RANDOM_3:def 8 :: thesis: F . n is SigmaField of (S . n)

n in NAT by ORDINAL1:def 12;

hence F . n is SigmaField of (S . n) by A2; :: thesis: verum