let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X holds
( (z ExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X )
let z, w be Element of X; :: thesis: ( (z ExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X )
thus (z ExpSeq) . 0 = (1r / (0 !)) * (z #N 0) by Def2
.= (1r / (0 !)) * ((z GeoSeq) . 0) by CLOPBAN3:def 8
.= 1r * (1. X) by CLOPBAN3:def 7, SIN_COS:1
.= 1. X by CLOPBAN3:38 ; :: thesis: (Expan (0,z,w)) . 0 = 1. X
A1: 0 -' 0 = 0 by XREAL_1:232;
hence (Expan (0,z,w)) . 0 = (((Coef 0) . 0) * (z #N 0)) * (w #N 0) by Def4
.= ((1r / (1r * 1r)) * (z #N 0)) * (w #N 0) by A1, COMPLEX1:def 4, SIN_COS:1, SIN_COS:def 6
.= (z #N 0) * (w #N 0) by CLOPBAN3:38, COMPLEX1:def 4
.= ((z GeoSeq) . 0) * (w #N 0) by CLOPBAN3:def 8
.= ((z GeoSeq) . 0) * ((w GeoSeq) . 0) by CLOPBAN3:def 8
.= (1. X) * ((w GeoSeq) . 0) by CLOPBAN3:def 7
.= (1. X) * (1. X) by CLOPBAN3:def 7
.= 1. X by CLOPBAN3:38 ;
:: thesis: verum