let th be Real; :: thesis: th rExpSeq = Re (th ExpSeq)
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
(Re (th ExpSeq)) . n = Re ((th ExpSeq) . n) by COMSEQ_3:def 5
.= Re ((th |^ n) / ((n !) + (0 * <i>))) by Def4
.= Re (((th |^ n) / (n !)) + (0 * <i>))
.= (th |^ n) / (n !) by COMPLEX1:12
.= (th rExpSeq) . n by Def5 ;
hence (th rExpSeq) . n = (Re (th ExpSeq)) . n ; :: thesis: verum
end;
hence th rExpSeq = Re (th ExpSeq) ; :: thesis: verum