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