let f1, f2 be Function of Omega,REAL; :: thesis: ( ( for w being Element of Omega holds f1 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n ) & ( for w being Element of Omega holds f2 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n ) implies f1 = f2 )
assume that
A1: for w being Element of Omega holds f1 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n and
A2: for w being Element of Omega holds f2 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n ; :: thesis: f1 = f2
let w be Element of Omega; :: according to FUNCT_2:def 8 :: thesis: f1 . w = f2 . w
f2 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n by A2;
hence f1 . w = f2 . w by A1; :: thesis: verum