let w, z be Complex; :: thesis: ( (z ExpSeq) . 0 = 1 & (Expan (0,z,w)) . 0 = 1 )
thus (z ExpSeq) . 0 = (z |^ 0) / (0 !) by Def4
.= 1 by Th1, COMSEQ_3:def 1 ; :: thesis: (Expan (0,z,w)) . 0 = 1
A1: 0 -' 0 = 0 by XREAL_1:232;
hence (Expan (0,z,w)) . 0 = (((Coef 0) . 0) * (z |^ 0)) * (w |^ 0) by Def9
.= ((1 / (1 * 1)) * (z |^ 0)) * (w |^ 0) by A1, Def6, Th1
.= 1r * ((w GeoSeq) . 0) by COMSEQ_3:def 1
.= 1 by COMSEQ_3:def 1 ;
:: thesis: verum