let F be Function of NAT , ExtREAL ; :: thesis: ( ( for n being Element of NAT holds F . n in REAL ) implies for n being Element of NAT holds (Ser F) . n in REAL )
assume A1: for n being Element of NAT holds F . n in REAL ; :: thesis: for n being Element of NAT holds (Ser F) . n in REAL
defpred S₁[ Element of NAT ] means (Ser F) . $1 in REAL ;
(Ser F) . 0 = F . 0 by Th63;
then A2: S₁[ 0 ] by A1;
A3: for s being Element of NAT st S₁[s] holds
S₁[s + 1]

proof

let s be Element of NAT ; :: thesis: ( S₁[s] implies S₁[s + 1] )
assume A4: (Ser F) . s in REAL ; :: thesis: S₁[s + 1]
reconsider y = (Ser F) . s as R_eal ;
A5: (Ser F) . (s + 1) = y + (F . (s + 1)) by Th63;
reconsider b = F . (s + 1) as Real by A1;
reconsider a = y as Real by A4;
y + (F . (s + 1)) = a + b by Th1;
hence S₁[s + 1] by A5; :: thesis: verum

end;

thus for s being Element of NAT holds S₁[s] from NAT_1:sch 1(A2, A3); :: thesis: verum