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
A1: len G = 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 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
A5: ( len F = len G & ( for j being Nat st j in dom F holds
F . j = H₁(j) ) ) from FINSEQ_2:sch 1();
A6: dom F = dom G by A5, FINSEQ_3:29;

A7: now

let n be Nat; :: thesis: ( n in dom F implies ((1 / (card Omega)) (#) G) . n = F . n )
assume A8: 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, A5, FINSEQ_1:def 3 ;
then s . n in Omega by A8, PARTFUN1:4;
then reconsider A = {(s . n)} as Singleton of Omega by RPR_1:4;
A9: (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)) * (X . (s . n)) by A4, A6, A8
.= F . n by A5, A8, A9 ; :: thesis: verum

end;

dom F = dom ((1 / (card Omega)) (#) G) by A6, VALUED_1:def 5;
then (1 / (card Omega)) (#) G = F by A7, FINSEQ_1:13;
then expect (X,(Trivial-Probability Omega)) = Sum ((1 / (card Omega)) (#) G) by A1, A2, A3, A5, Th31
.= (Sum G) / (card Omega) by RVSUM_1:87 ;
hence expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) ; :: thesis: verum