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