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 Def10;
Ser F = Ser ((rng F),N) by Def15;
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 Def11; :: thesis: verum