let k be Nat; :: thesis: for F being sequence of 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 sequence of 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 ) ) )
defpred S1[ Nat] means ( $1 < k implies (Ser F) . $1 = 0. );
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 ) )
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: ( n < k implies (Ser F) . n = 0. ) ; :: thesis: S1[n + 1]
assume A4: n + 1 < k ; :: thesis: (Ser F) . (n + 1) = 0.
then A5: ( n <= n + 1 & F . (n + 1) = 0. ) by A1, NAT_1:11;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:def 11
.= 0. by A3, A4, A5, XXREAL_0:2 ;
hence (Ser F) . (n + 1) = 0. ; :: thesis: verum
end;
A6: S1[ 0 ]
proof
assume 0 < k ; :: thesis: (Ser F) . 0 = 0.
then F . 0 = 0. by A1;
hence (Ser F) . 0 = 0. by SUPINF_2:def 11; :: thesis: verum
end;
A7: for n being Nat holds S1[n] from NAT_1:sch 2(A6, A2);
 defpred S2[ Nat] means ( k <= $1 implies (Ser F) . $1 = F . k );
A8: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A9: ( k <= n implies (Ser F) . n = F . k ) ; :: thesis: S2[n + 1]
assume A10: k <= n + 1 ; :: thesis: (Ser F) . (n + 1) = F . k
per cases ( k <= n or k = n + 1 ) by A10, NAT_1:8;
suppose A11: k <= n ; :: thesis: (Ser F) . (n + 1) = F . k
then k <> n + 1 by NAT_1:13;
then A12: F . (n + 1) = 0. by A1;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:def 11
.= F . k by A9, A11, A12, XXREAL_3:4 ;
hence (Ser F) . (n + 1) = F . k ; :: thesis: verum
end;
suppose A13: k = n + 1 ; :: thesis: (Ser F) . (n + 1) = F . k
then n < k by NAT_1:13;
then A14: (Ser F) . n = 0. by A7;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:def 11
.= F . k by A13, A14, XXREAL_3:4 ;
hence (Ser F) . (n + 1) = F . k ; :: thesis: verum
end;
end;
end;
A15: S2[ 0 ]
proof
A16: 0 <= k by NAT_1:2;
assume k <= 0 ; :: thesis: (Ser F) . 0 = F . k
then F . 0 = F . k by A16, XXREAL_0:1;
hence (Ser F) . 0 = F . k by SUPINF_2:def 11; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A15, A8);
 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 A7; :: thesis: verum