for X being Banach_Algebra
for w, z being Element of X holds
( (z rExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X )