let X be Complex_Banach_Algebra; :: thesis: exp (0. X) = 1. X
exp (0. X) = Sum ((0. X) ExpSeq) by Def6
.= 1. X by Th19 ;
hence exp (0. X) = 1. X ; :: thesis: verum