consider f being Function of Omega,REAL such that
B1: ( f = ChiFuncs . n & f is_random_variable_on F, Borel_Sets ) by RanDef;
thus ChiFuncs . n is random_variable of F, Borel_Sets by B1, RANDOM_3:def 1; :: thesis: verum