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
A1: len F = card Omega and
A2: ( s is one-to-one & rng s = Omega ) and
A3: len s = card Omega and
A4: for n being Nat st n in dom F holds
F . n = (X . (s . n)) * ((Trivial-Probability Omega) . {(s . n)}) and
A5: expect (X,(Trivial-Probability Omega)) = Sum F by Th33;
deffunc H₁( Nat) -> Element of REAL = In ((X . (s . $1)),REAL);
consider G being FinSequence of REAL such that
A6: ( len G = len F & ( for j being Nat st j in dom G holds
G . j = H₁(j) ) ) from FINSEQ_2:sch 1();
A7: dom F = dom G by A6, FINSEQ_3:29;

A8: now :: thesis: for n being Nat st n in dom F holds
((1 / (card Omega)) (#) G) . n = F . n

let n be Nat; :: thesis: ( n in dom F implies ((1 / (card Omega)) (#) G) . n = F . n )
assume A9: 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 A1, A3, FINSEQ_1:def 3 ;
then s . n in Omega by A9, PARTFUN1:4;
then reconsider A = {(s . n)} as Singleton of Omega by RPR_1:4;
A10: (Trivial-Probability Omega) . {(s . n)} = prob A by Def1
.= 1 / (card Omega) by RPR_1:14 ;
thus ((1 / (card Omega)) (#) G) . n = (1 / (card Omega)) * (G . n) by VALUED_1:6
.= (1 / (card Omega)) * H₁(n) by A6, A7, A9
.= (1 / (card Omega)) * (X . (s . n))
.= (X . (s . n)) * ((Trivial-Probability Omega) . {(s . n)}) by A10
.= F . n by A4, A9 ; :: thesis: verum

end;

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) )
take s ; :: thesis: ( 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) )
dom F = dom ((1 / (card Omega)) (#) G) by A7, VALUED_1:def 5;
then A11: (1 / (card Omega)) (#) G = F by A8, FINSEQ_1:13;
thus ( len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega ) by A1, A2, A3, A6; :: thesis: ( ( for n being Nat st n in dom G holds
G . n = X . (s . n) ) & expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) )
thus for n being Nat st n in dom G holds
G . n = X . (s . n) :: thesis: expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega)

proof

let n be Nat; :: thesis: ( n in dom G implies G . n = X . (s . n) )
assume n in dom G ; :: thesis: G . n = X . (s . n)
then G . n = H₁(n) by A6;
hence G . n = X . (s . n) ; :: thesis: verum

end;

Sum ((1 / (card Omega)) (#) G) = (1 / (card Omega)) * (Sum G) by RVSUM_1:87;
hence expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) by A5, A11, XCMPLX_1:99; :: thesis: verum