defpred S_{1}[ set , set ] means ex Dn being non empty set ex Sn being SigmaField of Dn st

( Dn = D . D & Sn = S . D & S is Probability of Sn );

set X = union (rng S);

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

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

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

let n be Nat; :: according to RANDOM_3:def 9 :: thesis: F . n is Probability of S . n

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

ex Dn being non empty set ex Sn being SigmaField of Dn st

( Dn = D . n1 & Sn = S . n1 & F . n1 is Probability of Sn ) by A3;

hence F . n is Probability of S . n ; :: thesis: verum

( Dn = D . D & Sn = S . D & S is Probability of Sn );

set X = union (rng S);

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

proof

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

dom S = NAT by PARTFUN1:def 2;

then A2: S . n c= union (rng S) by ZFMISC_1:74, FUNCT_1:3;

reconsider Sn = S . n as SigmaField of (D . n) ;

set Mn = the Probability of Sn;

the Probability of Sn in Funcs ((S . n),REAL) by FUNCT_2:8;

then ex f being Function st

( the Probability of Sn = f & dom f = S . n & rng f c= REAL ) by FUNCT_2:def 2;

then the Probability of Sn in PFuncs ((union (rng S)),REAL) by PARTFUN1:def 3, A2;

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

end;dom S = NAT by PARTFUN1:def 2;

then A2: S . n c= union (rng S) by ZFMISC_1:74, FUNCT_1:3;

reconsider Sn = S . n as SigmaField of (D . n) ;

set Mn = the Probability of Sn;

the Probability of Sn in Funcs ((S . n),REAL) by FUNCT_2:8;

then ex f being Function st

( the Probability of Sn = f & dom f = S . n & rng f c= REAL ) by FUNCT_2:def 2;

then the Probability of Sn in PFuncs ((union (rng S)),REAL) by PARTFUN1:def 3, A2;

hence ex y being Element of PFuncs ((union (rng S)),REAL) st S

A3: for n being Element of NAT holds S

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

let n be Nat; :: according to RANDOM_3:def 9 :: thesis: F . n is Probability of S . n

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

ex Dn being non empty set ex Sn being SigmaField of Dn st

( Dn = D . n1 & Sn = S . n1 & F . n1 is Probability of Sn ) by A3;

hence F . n is Probability of S . n ; :: thesis: verum