exp_R . 0 = Sum (0 rExpSeq) by Def22
.= 1 by Th9, Th44, COMPLEX1:6 ;
hence exp_R . 0 = 1 ; :: thesis: verum