consider f being Function of Omega,REAL such that
B10: f = simple_RV_help (ChiFuncs,ConstFuncs,n) ;
f is random_variable of F, Borel_Sets

proof

defpred S₁[ Nat] means simple_RV_help (ChiFuncs,ConstFuncs,$1) is random_variable of F, Borel_Sets ;
set RVs0 = simple_RV_help (ChiFuncs,ConstFuncs,0);
J0: S₁[ 0 ]

proof

for w being Element of Omega holds (simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv_RV (ConstFuncs,0)) (#) (Conv_RV (ChiFuncs,0))) . w

proof

let w be Element of Omega; :: thesis: (simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv_RV (ConstFuncs,0)) (#) (Conv_RV (ChiFuncs,0))) . w
(simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . 0 by Def777;
then (simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w))) . 0 by SERIES_1:def 1;
then C2: (simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv2_RV (ConstFuncs,w)) . 0) * ((Conv2_RV (ChiFuncs,w)) . 0) by VALUED_1:5;
C3: (Conv2_RV (ConstFuncs,w)) . 0 = (Conv_RV (ConstFuncs,0)) . w by Def770;
(Conv2_RV (ChiFuncs,w)) . 0 = (Conv_RV (ChiFuncs,0)) . w by Def770;
hence (simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv_RV (ConstFuncs,0)) (#) (Conv_RV (ChiFuncs,0))) . w by VALUED_1:5, C2, C3; :: thesis: verum

end;

then simple_RV_help (ChiFuncs,ConstFuncs,0) = (Conv_RV (ConstFuncs,0)) (#) (Conv_RV (ChiFuncs,0)) ;
hence S₁[ 0 ] by FINANCE2:25; :: thesis: verum

end;

J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume ASS0: S₁[n] ; :: thesis: S₁[n + 1]
set RVsn = simple_RV_help (ChiFuncs,ConstFuncs,n);
set RVsn1 = simple_RV_help (ChiFuncs,ConstFuncs,(n + 1));
set RVa = (Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1)));
for w being Element of Omega holds (simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) + ((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))))) . w

proof

let w be Element of Omega; :: thesis: (simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) + ((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))))) . w
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . (n + 1) by Def777;
then (simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = (In (((Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n),REAL)) + (((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w))) . (n + 1)) by SERIES_1:def 1;
then (simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) . w) + (((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w))) . (n + 1)) by Def777;
then D1: (simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) . w) + (((Conv2_RV (ConstFuncs,w)) . (n + 1)) * ((Conv2_RV (ChiFuncs,w)) . (n + 1))) by VALUED_1:5;
D2: (Conv2_RV (ConstFuncs,w)) . (n + 1) = (Conv_RV (ConstFuncs,(n + 1))) . w by Def770;
(Conv2_RV (ChiFuncs,w)) . (n + 1) = (Conv_RV (ChiFuncs,(n + 1))) . w by Def770;
then (simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) . w) + (((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1)))) . w) by VALUED_1:5, D1, D2;
hence (simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) + ((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))))) . w by VALUED_1:1; :: thesis: verum

end;

then M1: simple_RV_help (ChiFuncs,ConstFuncs,(n + 1)) = (simple_RV_help (ChiFuncs,ConstFuncs,n)) + ((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1)))) ;
( simple_RV_help (ChiFuncs,ConstFuncs,n) is random_variable of F, Borel_Sets & (Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))) is random_variable of F, Borel_Sets ) by ASS0, FINANCE2:25;
hence S₁[n + 1] by M1, FINANCE2:23; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(J0, J1);
hence f is random_variable of F, Borel_Sets by B10; :: thesis: verum

end;

hence simple_RV_help (ChiFuncs,ConstFuncs,n) is random_variable of F, Borel_Sets by B10; :: thesis: verum