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