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