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

( 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