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