let S be non empty finite set ; :: thesis: 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) ) )
let s be non empty FinSequence of S; :: thesis: 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) ) )
reconsider n = len s as non empty Element of NAT ;
reconsider G = s as random_variable of Trivial-SigmaField (Seg (len s)), Trivial-SigmaField S by Th16;
take G ; :: thesis: ( G = s & ( for x being set st x in S holds
(probability (G,(Trivial-Probability (Seg (len s))))) . {x} = FDprobability (x,s) ) )
thus G = s ; :: thesis: for x being set st x in S holds
(probability (G,(Trivial-Probability (Seg (len s))))) . {x} = FDprobability (x,s)
let x be set ; :: thesis: ( x in S implies (probability (G,(Trivial-Probability (Seg (len s))))) . {x} = FDprobability (x,s) )
assume A1: x in S ; :: thesis: (probability (G,(Trivial-Probability (Seg (len s))))) . {x} = FDprobability (x,s)
set y = {x};
{x} c= S by A1, ZFMISC_1:31;
then (probability (G,(Trivial-Probability (Seg (len s))))) . {x} = (card (G " {x})) / (card (Seg (len s))) by Th17
.= (card (G " {x})) / n by FINSEQ_1:57 ;
hence (probability (G,(Trivial-Probability (Seg (len s))))) . {x} = FDprobability (x,s) ; :: thesis: verum