let k be Element of NAT ; :: thesis: for F being Function of NAT ,ExtREAL st ( for n being Element of NAT st n <> k holds
F . n = 0. ) holds
( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) )
let F be Function of NAT ,ExtREAL ; :: thesis: ( ( for n being Element of NAT st n <> k holds
F . n = 0. ) implies ( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) ) )
assume A1: for n being Element of NAT st n <> k holds
F . n = 0. ; :: thesis: ( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) )
defpred S₁[ Element of NAT ] means ( $1 < k implies (Ser F) . $1 = 0. );
A2: S₁[ 0 ]

proof

assume 0 < k ; :: thesis: (Ser F) . 0 = 0.
then F . 0 = 0. by A1;
hence (Ser F) . 0 = 0. by SUPINF_2:63; :: thesis: verum

end;

A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: ( n < k implies (Ser F) . n = 0. ) ; :: thesis: S₁[n + 1]
assume A5: n + 1 < k ; :: thesis: (Ser F) . (n + 1) = 0.
A6: n <= n + 1 by NAT_1:11;
A7: F . (n + 1) = 0. by A1, A5;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:63
.= 0. by A4, A5, A6, A7, XXREAL_0:2, XXREAL_3:4 ;
hence (Ser F) . (n + 1) = 0. ; :: thesis: verum

end;

A8: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
defpred S₂[ Element of NAT ] means ( k <= $1 implies (Ser F) . $1 = F . k );
A9: S₂[ 0 ]

proof

assume k <= 0 ; :: thesis: (Ser F) . 0 = F . k
then ( k <= 0 & 0 <= k ) by NAT_1:2;
then F . 0 = F . k by XXREAL_0:1;
hence (Ser F) . 0 = F . k by SUPINF_2:63; :: thesis: verum

end;

A10: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A11: ( k <= n implies (Ser F) . n = F . k ) ; :: thesis: S₂[n + 1]
assume A12: k <= n + 1 ; :: thesis: (Ser F) . (n + 1) = F . k

per cases ( k <= n or k = n + 1 ) by A12, NAT_1:8;

suppose A13: k <= n ; :: thesis: (Ser F) . (n + 1) = F . k

then k <> n + 1 by NAT_1:13;
then A14: F . (n + 1) = 0. by A1;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:63
.= F . k by A11, A13, A14, XXREAL_3:4 ;
hence (Ser F) . (n + 1) = F . k ; :: thesis: verum

end;

suppose A15: k = n + 1 ; :: thesis: (Ser F) . (n + 1) = F . k

then n < k by NAT_1:13;
then A16: (Ser F) . n = 0. by A8;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:63
.= F . k by A15, A16, XXREAL_3:4 ;
hence (Ser F) . (n + 1) = F . k ; :: thesis: verum

end;

end;

end;

for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A9, A10);
hence ( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) ) by A8; :: thesis: verum