theorem Th7: :: SIN_COS:7
for w, z being Complex
for n being Nat holds Expan_e (n,z,w) = (1r / (n !)) (#) (Expan (n,z,w))