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

now :: thesis: ( 0 >= i & 0 >= j implies (Ser f) . 0 = (Ser g) . 0 )

assume ( 0 >= i & 0 >= j ) ; :: thesis: (Ser f) . 0 = (Ser g) . 0
then ( i = 0 & j = 0 ) ;
then (Ser f) . 0 = g . 0 by A2, SUPINF_2:def 11;
hence (Ser f) . 0 = (Ser g) . 0 by SUPINF_2:def 11; :: thesis: verum

end;

then A6: S₁[ 0 ] ;
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( k + 1 >= i & k + 1 >= j implies (Ser f) . (k + 1) = (Ser g) . (k + 1) )

assume A9: ( k + 1 >= i & k + 1 >= j ) ; :: thesis: (Ser f) . (k + 1) = (Ser g) . (k + 1)

per cases ( ( k < i & k < j ) or ( k >= i & k < j ) or ( k < i & k >= j ) or ( k >= i & k >= j ) ) ;

suppose ( k < i & k < j ) ; :: thesis: (Ser f) . (k + 1) = (Ser g) . (k + 1)

then ( k + 1 <= i & k + 1 <= j ) by NAT_1:13;
then ( k + 1 = i & k + 1 = j ) by A9, XXREAL_0:1;
hence (Ser f) . (k + 1) = (Ser g) . (k + 1) by A1, A3, A4, Th49; :: thesis: verum

end;

suppose A10: ( k >= i & k < j ) ; :: thesis: (Ser f) . (k + 1) = (Ser g) . (k + 1)

then k + 1 <= j by NAT_1:13;
then A11: k + 1 = j by A9, XXREAL_0:1;
for n being Nat st n <> j & n <> i holds
f . n = g . n by A4;
hence (Ser f) . (k + 1) = (Ser g) . (k + 1) by A1, A2, A3, A11, A10, NAT_1:12, Th49; :: thesis: verum

end;

suppose A12: ( k < i & k >= j ) ; :: thesis: (Ser f) . (k + 1) = (Ser g) . (k + 1)

then k + 1 <= i by NAT_1:13;
then k + 1 = i by A9, XXREAL_0:1;
hence (Ser f) . (k + 1) = (Ser g) . (k + 1) by A1, A2, A3, A4, A12, NAT_1:12, Th49; :: thesis: verum

end;

suppose A13: ( k >= i & k >= j ) ; :: thesis: (Ser f) . (k + 1) = (Ser g) . (k + 1)

then A14: ( k + 1 > i & k + 1 > j ) by NAT_1:13;
(Ser f) . (k + 1) = ((Ser f) . k) + (f . (k + 1)) by SUPINF_2:def 11
.= ((Ser g) . k) + (g . (k + 1)) by A4, A8, A13, A14 ;
hence (Ser f) . (k + 1) = (Ser g) . (k + 1) by SUPINF_2:def 11; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A7);
hence (Ser f) . n = (Ser g) . n by A5; :: thesis: verum