theorem Th17: :: CLOPBAN4:17

for X being Complex_Banach_Algebra
for w, z being Element of X
for n being Nat holds Expan_e (n,z,w) = (1r / (n !)) * (Expan (n,z,w))