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 = In (((X . (s . $1)) * ((Trivial-Probability Omega) . {(s . $1)})),REAL);
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;
reconsider cG = (1 / (card Omega)) (#) G as FinSequence of REAL by RVSUM_1:145;
A7: dom F = dom cG by A6, VALUED_1:def 5;
A8: for n being Nat st n in dom cG holds
cG . n = F . n

proof

let n be Nat; :: thesis: ( n in dom cG implies cG . n = F . n )
assume A9: n in dom cG ; :: thesis: cG . 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 A9, PARTFUN1:4, A7;
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 cG . n = (1 / (card Omega)) * (G . n) by VALUED_1:6
.= (1 / (card Omega)) * (X . (s . n)) by A4, A6, A9, A7
.= H₁(n) by A10
.= F . n by A5, A9, A7 ; :: thesis: verum

end;

A11: for n being Nat st n in dom cG holds
cG . n = (X . (s . n)) * ((Trivial-Probability Omega) . {(s . n)})

proof

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

end;

dom F = dom ((1 / (card Omega)) (#) G) by A6, VALUED_1:def 5;
then A14: (1 / (card Omega)) (#) G = F by FINSEQ_1:13, A8;
A15: len cG = card Omega by A1, A5, A14;
A16: s is one-to-one by A2;
( rng s = Omega & len s = card Omega ) by A2, A3;
then expect (X,(Trivial-Probability Omega)) = Sum cG by Th31, A15, A16, A11;
then expect (X,(Trivial-Probability Omega)) = Sum cG
.= Sum ((1 / (card Omega)) (#) G)
.= (1 / (card Omega)) * (Sum G) by RVSUM_1:87
.= (Sum G) / (card Omega) by XCMPLX_1:99 ;
hence expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) ; :: thesis: verum