let X be Banach_Algebra; :: thesis: for w, z being Element of X
for k being Nat holds (z rExpSeq) . k = (Expan_e (k,z,w)) . k
let w, z be Element of X; :: thesis: for k being Nat holds (z rExpSeq) . k = (Expan_e (k,z,w)) . k
let k be Nat; :: thesis: (z rExpSeq) . k = (Expan_e (k,z,w)) . k
A1: 0 = k - k ;
then A2: (k -' k) ! = 1 by NEWTON:12, XREAL_1:233;
k -' k = 0 by A1, XREAL_1:233;
hence (Expan_e (k,z,w)) . k = (((Coef_e k) . k) * (z #N k)) * (w #N 0) by Def7
.= (((Coef_e k) . k) * (z #N k)) * (1. X) by LOPBAN_3:39
.= ((Coef_e k) . k) * (z #N k) by LOPBAN_3:38
.= (1 / ((k !) * 1)) * (z #N k) by A2, Def4
.= (z rExpSeq) . k by Def2 ;
:: thesis: verum