let X be Banach_Algebra; :: thesis: exp (0. X) = 1. X
exp (0. X) = Sum ((0. X) rExpSeq) by Def10
.= 1. X by Th20 ;
hence exp (0. X) = 1. X ; :: thesis: verum