let f, g be sequence of ExtREAL; :: thesis: for i, j being Nat st f is V115() & 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 V115() & 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 V115() 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 S1[ 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: S1[ 0 ] ;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[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 S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A6, A7);
 hence (Ser f) . n = (Ser g) . n by A5; :: thesis: verum