deffunc H₁( Element of Omega) -> Element of REAL = In (((Partial_Sums ((Conv2_RV (ConstFuncs,$1)) (#) (Conv2_RV (ChiFuncs,$1)))) . n),REAL);
consider f being Function of Omega,REAL such that
A1: for d being Element of Omega holds f . d = H₁(d) from FUNCT_2:sch 4();
take f ; :: thesis: for w being Element of Omega holds f . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n
let w be Element of Omega; :: thesis: f . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n
In (((Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n),REAL) = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n ;
hence f . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n by A1; :: thesis: verum