let F be Function of NAT,ExtREAL; :: thesis: ( (Ser F) . 0 = F . 0 & ( for n being Element of NAT
for y being R_eal st y = (Ser F) . n holds
(Ser F) . (n + 1) = y + (F . (n + 1)) ) )
reconsider N = F as Num of rng F by Def16;
Ser F = Ser ((rng F),N) by Def21;
hence ( (Ser F) . 0 = F . 0 & ( for n being Element of NAT
for y being R_eal st y = (Ser F) . n holds
(Ser F) . (n + 1) = y + (F . (n + 1)) ) ) by Def17; :: thesis: verum