let Omega be non empty finite set ; :: thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega
for G being FinSequence of REAL
for 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) ) holds
expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega)
let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; :: thesis: for G being FinSequence of REAL
for 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) ) holds
expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega)
let G be FinSequence of REAL ; :: thesis: for 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) ) holds
expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega)
let s be FinSequence of Omega; :: 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) ) implies expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega) )
assume that
AS0: len G = card Omega and
AS0a: s is one-to-one and
AS0b: ( rng s = Omega & len s = card Omega ) and
AS0c: 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)
set P = Trivial-Probability Omega;
deffunc H₁( Nat) -> Element of REAL = (X . (s . $1)) * ((Trivial-Probability Omega) . {(s . $1)});
consider F being FinSequence of REAL such that
P2: ( len F = len G & ( for j being Nat st j in dom F holds
F . j = H₁(j) ) ) from FINSEQ_2:sch 1();
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 AS1: 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, AS0, AS0b, P2 ;
then s . n in Omega by PARTFUN1:27, AS1;
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 P4, AS1, AS0c
.= F . n by P3, P2, AS1 ; :: thesis: verum

end;

then (1 / (card Omega)) (#) G = F by FINSEQ_1:17, P7;
then expect X,(Trivial-Probability Omega) = Sum ((1 / (card Omega)) (#) G) by LMTX4, P2, AS0, AS0a, AS0b
.= (Sum G) / (card Omega) by RVSUM_1:117 ;
hence expect X,(Trivial-Probability Omega) = (Sum G) / (card Omega) ; :: thesis: verum