let X be Complex_Banach_Algebra; :: thesis: for w, z being Element of X holds
( (z ExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X )
let w, z 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 Def1
.= (1r / (0 !)) * ((z GeoSeq) . 0) by CLOPBAN3:def 8
.= 1r * (1. X) by CLOPBAN3:def 7, SIN_COS:1
.= 1. X by CLVECT_1:def 5 ; :: 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 Def2
.= ((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 CLVECT_1:def 5, 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 VECTSP_1:def 4 ;
:: thesis: verum