let X be Banach_Algebra; :: thesis: for z, w being Element of X holds
( (z rExpSeq ) . 0 = 1. X & (Expan 0 ,z,w) . 0 = 1. X )
let z, w be Element of X; :: thesis: ( (z rExpSeq ) . 0 = 1. X & (Expan 0 ,z,w) . 0 = 1. X )
thus (z rExpSeq ) . 0 = (1 / (0 ! )) * (z #N 0 ) by Def2
.= (1 / 1) * (1. X) by LOPBAN_3:def 13, NEWTON:18
.= 1. X by LOPBAN_3:43 ; :: 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 Def6
.= ((1 / (1 * 1)) * (z #N 0 )) * (w #N 0 ) by A1, Def3, NEWTON:18
.= ((z GeoSeq ) . 0 ) * (w #N 0 ) by LOPBAN_3:43
.= (1. X) * ((w GeoSeq ) . 0 ) by LOPBAN_3:def 13
.= (1. X) * (1. X) by LOPBAN_3:def 13
.= 1. X by LOPBAN_3:43 ;
:: thesis: verum