A1: exp_R . 0 = Sum (0 rExpSeq ) by Def26
.= 1 by Th10, Th49, COMPLEX1:15 ;
thus exp_R . 0 = 1 by A1; :: thesis: verum