let z, w be Element of COMPLEX ; :: thesis: ( (z ExpSeq ) . 0 = 1 & (Expan 0 ,z,w) . 0 = 1 )
thus (z ExpSeq ) . 0 = (z |^ 0 ) / (0 !c ) by Def8
.= 1 by Th1, COMSEQ_3:def 1 ; :: thesis: (Expan 0 ,z,w) . 0 = 1
A1: 0 -' 0 = 0 by XREAL_1:234;
thus (Expan 0 ,z,w) . 0 = (((Coef 0 ) . 0 ) * (z |^ 0 )) * (w |^ 0 ) by A1, Def13
.= ((1 / (1 * 1)) * (z |^ 0 )) * (w |^ 0 ) by A1, Def10, Th1
.= 1r * ((w GeoSeq ) . 0 ) by COMSEQ_3:def 1
.= 1 by COMSEQ_3:def 1 ; :: thesis: verum