let Omega be non empty finite set ; 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); 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 H1( 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 = H1(j) ) )
from FINSEQ_2:sch 1();
A7:
dom F = dom G
by A6, FINSEQ_3:29;
take
G
; 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
; ( 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; ( ( 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)
expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega)
thus
expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega)
by A5, RVSUM_1:87, A11; verum