defpred S₁[ 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₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of PFuncs ((union (rng S)),REAL) st S₁[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₁[n,y] ; :: thesis: verum

end;

consider F being Function of NAT,(PFuncs ((union (rng S)),REAL)) such that
A3: for n being Element of NAT holds S₁[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