let th be Real; :: thesis: th rExpSeq = Re (th ExpSeq )
A1: for n being Element of NAT holds (th rExpSeq ) . n = (Re (th ExpSeq )) . n

proof

let n be Element of NAT ; :: thesis: (th rExpSeq ) . n = (Re (th ExpSeq )) . n
A2: (Re (th ExpSeq )) . n = Re ((th ExpSeq ) . n) by COMSEQ_3:def 3
.= Re ((th |^ n) / ((n !c ) + (0 * <i> ))) by Def8
.= Re (((th |^ n) / (n ! )) + (0 * <i> )) by Th37
.= (th |^ n) / (n ! ) by COMPLEX1:28
.= (th rExpSeq ) . n by Def9 ;
thus (th rExpSeq ) . n = (Re (th ExpSeq )) . n by A2; :: thesis: verum

end;

thus th rExpSeq = Re (th ExpSeq ) by A1, FUNCT_2:113; :: thesis: verum