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