let Omega be non empty finite set ; :: thesis:
let X be Real-Valued-Random-Variable of (Trivial-SigmaField Omega); :: thesis:
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;

let n be Nat; :: thesis:
assume A9: n in dom F ; :: thesis:
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:

end;

take G ; :: thesis:
take s ; :: thesis:
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:
thus for n being Nat st n in dom G holds
G . n = X . (s . n) :: thesis:

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

end;