let f, g be sequence of ExtREAL; :: thesis: for j, k being Nat st k < j & ( for n being Nat st n < j holds
f . n = g . n ) holds
(Ser f) . k = (Ser g) . k
let j, k be Nat; :: thesis: ( k < j & ( for n being Nat st n < j holds
f . n = g . n ) implies (Ser f) . k = (Ser g) . k )
assume that
A1: k < j and
A2: for n being Nat st n < j holds
f . n = g . n ; :: thesis: (Ser f) . k = (Ser g) . k
defpred S₁[ Nat] means ( $1 <= k implies (Ser f) . $1 = (Ser g) . $1 );

now :: thesis: ( 0 <= k implies (Ser f) . 0 = (Ser g) . 0 )

assume 0 <= k ; :: thesis: (Ser f) . 0 = (Ser g) . 0
f . 0 = g . 0 by A1, A2;
then (Ser f) . 0 = g . 0 by SUPINF_2:def 11;
hence (Ser f) . 0 = (Ser g) . 0 by SUPINF_2:def 11; :: thesis: verum

end;

then A3: S₁[ 0 ] ;
A4: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: S₁[m] ; :: thesis: S₁[m + 1]
assume A6: m + 1 <= k ; :: thesis: (Ser f) . (m + 1) = (Ser g) . (m + 1)
then A7: m + 1 < j by A1, XXREAL_0:2;
(Ser f) . (m + 1) = ((Ser f) . m) + (f . (m + 1)) by SUPINF_2:def 11;
then (Ser f) . (m + 1) = ((Ser g) . m) + (g . (m + 1)) by A2, A5, A6, A7, NAT_1:13;
hence (Ser f) . (m + 1) = (Ser g) . (m + 1) by SUPINF_2:def 11; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A3, A4);
hence (Ser f) . k = (Ser g) . k ; :: thesis: verum