let X be Banach_Algebra; :: thesis: for z, w being Element of X
for k being Element of NAT holds (z rExpSeq ) . k = (Expan_e k,z,w) . k
let z, w be Element of X; :: thesis: for k being Element of NAT holds (z rExpSeq ) . k = (Expan_e k,z,w) . k
let k be Element of NAT ; :: thesis: (z rExpSeq ) . k = (Expan_e k,z,w) . k
A1: 0 = k - k ;
then A2: k -' k = 0 by XREAL_1:235;
A3: (k -' k) ! = 1 by A1, NEWTON:18, XREAL_1:235;
thus (Expan_e k,z,w) . k = (((Coef_e k) . k) * (z #N k)) * (w #N 0 ) by A2, Def7
.= (((Coef_e k) . k) * (z #N k)) * (1. X) by LOPBAN_3:44
.= ((Coef_e k) . k) * (z #N k) by LOPBAN_3:43
.= (1 / ((k ! ) * 1)) * (z #N k) by A3, Def4
.= (z rExpSeq ) . k by Def2 ; :: thesis: verum