theorem :: RANDOM_3:18

for S being non empty finite set
for s being non empty FinSequence of S ex G being random_variable of Trivial-SigmaField (Seg (len s)), Trivial-SigmaField S st
( G = s & ( for x being set st x in S holds
(probability (G,(Trivial-Probability (Seg (len s))))) . {x} = FDprobability (x,s) ) )