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