let Omega be non empty finite set ; :: thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex G being FinSequence of REAL ex s being FinSequence of Omega st
( len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom G holds
G . n = X . (s . n) ) & expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega) )
let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; :: thesis: ex G being FinSequence of REAL ex s being FinSequence of Omega st
( len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom G holds
G . n = X . (s . n) ) & expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega) )
set P = Trivial-Probability Omega;
consider F being FinSequence of REAL , s being FinSequence of Omega such that
P1: ( len F = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom F holds
F . n = (X . (s . n)) * ((Trivial-Probability Omega) . {(s . n)}) ) & expect X,(Trivial-Probability Omega) = Sum F ) by LMTX5;
deffunc H₁( Nat) -> Element of REAL = X . (s . $1);
consider G being FinSequence of REAL such that
P2: ( len G = len F & ( for j being Nat st j in dom G holds
G . j = H₁(j) ) ) from FINSEQ_2:sch 1();
take G ; :: thesis: ex s being FinSequence of Omega st
( len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom G holds
G . n = X . (s . n) ) & expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega) )
P4: dom F = dom G by FINSEQ_3:31, P2;
then P7: dom F = dom ((1 / (card Omega)) (#) G) by VALUED_1:def 5;

now

let n be Nat; :: thesis: ( n in dom F implies ((1 / (card Omega)) (#) G) . n = F . n )
assume AS0: n in dom F ; :: thesis: ((1 / (card Omega)) (#) G) . n = F . n
dom s = Seg (len s) by FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3, P1 ;
then s . n in Omega by PARTFUN1:27, AS0;
then reconsider A = {(s . n)} as El_ev of Omega by RPR_1:7;
P3: (Trivial-Probability Omega) . {(s . n)} = prob A by defTP
.= 1 / (card Omega) by RPR_1:38 ;
thus ((1 / (card Omega)) (#) G) . n = (1 / (card Omega)) * (G . n) by VALUED_1:6
.= (1 / (card Omega)) * (X . (s . n)) by P2, P4, AS0
.= F . n by AS0, P1, P3 ; :: thesis: verum

end;

then (1 / (card Omega)) (#) G = F by FINSEQ_1:17, P7;
hence ex s being FinSequence of Omega st
( len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom G holds
G . n = X . (s . n) ) & expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega) ) by P1, P2, RVSUM_1:117; :: thesis: verum