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 !c )) * (z #N 0 ) by Def2
.= (1r / (0 !c )) * ((z GeoSeq ) . 0 ) by CLOPBAN3:def 13
.= 1r * (1. X) by CLOPBAN3:def 12, SIN_COS:1
.= 1. X by CLOPBAN3:42 ; :: thesis: (Expan 0 ,z,w) . 0 = 1. X
A1: 0 -' 0 = 0 by XREAL_1:234;
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 7, SIN_COS:1, SIN_COS:def 10
.= (z #N 0 ) * (w #N 0 ) by CLOPBAN3:42, COMPLEX1:def 7
.= ((z GeoSeq ) . 0 ) * (w #N 0 ) by CLOPBAN3:def 13
.= ((z GeoSeq ) . 0 ) * ((w GeoSeq ) . 0 ) by CLOPBAN3:def 13
.= (1. X) * ((w GeoSeq ) . 0 ) by CLOPBAN3:def 12
.= (1. X) * (1. X) by CLOPBAN3:def 12
.= 1. X by CLOPBAN3:42 ;
:: thesis: verum