let f, g be sequence of ExtREAL; :: thesis: for i, j being Nat st f is nonnegative & i >= j & ( for n being Nat st n <> i & n <> j holds
f . n = g . n ) & f . i = g . j & f . j = g . i holds
(Ser f) . i = (Ser g) . i
let i, j be Nat; :: thesis: ( f is nonnegative & i >= j & ( for n being Nat st n <> i & n <> j holds
f . n = g . n ) & f . i = g . j & f . j = g . i implies (Ser f) . i = (Ser g) . i )
assume that
A1: f is nonnegative and
A2: i >= j and
A3: for n being Nat st n <> i & n <> j holds
f . n = g . n and
A4: f . i = g . j and
A5: f . j = g . i ; :: thesis: (Ser f) . i = (Ser g) . i
A6: for k being Element of NAT holds 0 <= g . k

proof

let k be Element of NAT ; :: thesis: 0 <= g . k

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

suppose ( k = i or k = j ) ; :: thesis: 0 <= g . k

hence 0 <= g . k by A1, A4, A5, SUPINF_2:51; :: thesis: verum

end;

suppose ( k <> i & k <> j ) ; :: thesis: 0 <= g . k

then g . k = f . k by A3;
hence 0 <= g . k by A1, SUPINF_2:51; :: thesis: verum

end;

end;

end;

then A7: g is nonnegative by SUPINF_2:39;

per cases ( j = 0 or j <> 0 ) ;

suppose A8: j = 0 ; :: thesis: (Ser f) . i = (Ser g) . i

defpred S₁[ Nat] means ( $1 < i implies ((Ser f) . $1) + (f . i) = ((Ser g) . $1) + (g . i) );

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

assume 0 < i ; :: thesis: ((Ser f) . 0) + (f . i) = ((Ser g) . 0) + (g . i)
( f . i = (Ser g) . 0 & (Ser f) . 0 = g . i ) by A4, A5, A8, SUPINF_2:def 11;
hence ((Ser f) . 0) + (f . i) = ((Ser g) . 0) + (g . i) ; :: thesis: verum

end;

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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A11: S₁[m] ; :: thesis: S₁[m + 1]
assume A12: m + 1 < i ; :: thesis: ((Ser f) . (m + 1)) + (f . i) = ((Ser g) . (m + 1)) + (g . i)
A13: ( 0 <= f . m & 0 <= f . (m + 1) & 0 <= f . i ) by A1, SUPINF_2:51;
then A14: 0 <= (Ser f) . m by A1, MEASURE7:2;
A15: ( 0 <= g . m & 0 <= g . (m + 1) & 0 <= g . i ) by A6, SUPINF_2:39, SUPINF_2:51;
then A16: 0 <= (Ser g) . m by A7, MEASURE7:2;
A17: f . (m + 1) = g . (m + 1) by A3, A8, A12;
then A18: ( (Ser f) . (m + 1) = (g . (m + 1)) + ((Ser f) . m) & (Ser g) . (m + 1) = (f . (m + 1)) + ((Ser g) . m) ) by SUPINF_2:def 11;
then ((Ser f) . (m + 1)) + (f . i) = (g . (m + 1)) + (((Ser f) . m) + (f . i)) by A13, A14, A15, XXREAL_3:44;
hence ((Ser f) . (m + 1)) + (f . i) = ((Ser g) . (m + 1)) + (g . i) by A11, A12, A15, A16, A17, A18, XXREAL_3:44, NAT_1:13; :: thesis: verum

end;

A19: for m being Nat holds S₁[m] from NAT_1:sch 2(A9, A10);

per cases ( i = 0 or i <> 0 ) ;

suppose A20: i = 0 ; :: thesis: (Ser f) . i = (Ser g) . i

then ( (Ser f) . i = f . 0 & (Ser g) . i = g . 0 ) by SUPINF_2:def 11;
hence (Ser f) . i = (Ser g) . i by A4, A8, A20; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: (Ser f) . i = (Ser g) . i

then reconsider m = i - 1 as Nat by NAT_1:20;
A21: i = m + 1 ;
then m < i by NAT_1:13;
then ((Ser f) . m) + (f . i) = ((Ser g) . m) + (g . i) by A19;
then (Ser f) . i = ((Ser g) . m) + (g . i) by A21, SUPINF_2:def 11;
hence (Ser f) . i = (Ser g) . i by A21, SUPINF_2:def 11; :: thesis: verum

end;

end;

end;

suppose A22: j <> 0 ; :: thesis: (Ser f) . i = (Ser g) . i

then reconsider m = j - 1 as Nat by NAT_1:20;
A23: j = m + 1 ;
then A24: m < j by NAT_1:13;
for n being Nat st n < j holds
f . n = g . n by A2, A3;
then A25: (Ser f) . m = (Ser g) . m by A24, Th48;

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

suppose A26: j = i ; :: thesis: (Ser f) . i = (Ser g) . i

then (Ser f) . i = ((Ser g) . m) + (g . i) by A4, A23, A25, SUPINF_2:def 11;
hence (Ser f) . i = (Ser g) . i by A23, A26, SUPINF_2:def 11; :: thesis: verum

end;

suppose j <> i ; :: thesis: (Ser f) . i = (Ser g) . i

then A27: j < i by A2, XXREAL_0:1;
defpred S₁[ Nat] means ( j <= $1 & $1 < i implies ((Ser f) . $1) + (f . i) = ((Ser g) . $1) + (g . i) );
A28: S₁[ 0 ] by A22;
A29: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A30: S₁[k] ; :: thesis: S₁[k + 1]
assume A31: ( j <= k + 1 & k + 1 < i ) ; :: thesis: ((Ser f) . (k + 1)) + (f . i) = ((Ser g) . (k + 1)) + (g . i)

per cases ( j = k + 1 or j <> k + 1 ) ;

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

A33: ( 0 <= f . i & 0 <= g . i & 0 <= g . k ) by A1, A6, SUPINF_2:39, SUPINF_2:51;
then A34: 0 <= (Ser g) . k by A7, MEASURE7:2;
((Ser f) . (k + 1)) + (f . i) = (((Ser f) . k) + (f . (k + 1))) + (f . i) by SUPINF_2:def 11;
then ((Ser f) . (k + 1)) + (f . i) = (((Ser g) . k) + (f . i)) + (g . i) by A5, A25, A32, A33, A34, XXREAL_3:44;
hence ((Ser f) . (k + 1)) + (f . i) = ((Ser g) . (k + 1)) + (g . i) by A4, A32, SUPINF_2:def 11; :: thesis: verum

end;

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

then A35: j < k + 1 by A31, XXREAL_0:1;
A36: ( 0 <= f . (k + 1) & 0 <= f . i & 0 <= f . k ) by A1, SUPINF_2:51;
then A37: 0 <= (Ser f) . k by A1, MEASURE7:2;
A38: ( 0 <= g . (k + 1) & 0 <= g . i & 0 <= g . k ) by A6, SUPINF_2:39, SUPINF_2:51;
then A39: 0 <= (Ser g) . k by A7, MEASURE7:2;
(Ser f) . (k + 1) = (f . (k + 1)) + ((Ser f) . k) by SUPINF_2:def 11;
then ((Ser f) . (k + 1)) + (f . i) = (f . (k + 1)) + (((Ser f) . k) + (f . i)) by A36, A37, XXREAL_3:44;
then ((Ser f) . (k + 1)) + (f . i) = (g . (k + 1)) + (((Ser g) . k) + (g . i)) by A3, A30, A31, A35, NAT_1:13;
then ((Ser f) . (k + 1)) + (f . i) = ((g . (k + 1)) + ((Ser g) . k)) + (g . i) by A38, A39, XXREAL_3:44;
hence ((Ser f) . (k + 1)) + (f . i) = ((Ser g) . (k + 1)) + (g . i) by SUPINF_2:def 11; :: thesis: verum

end;

end;

end;

A40: for k being Nat holds S₁[k] from NAT_1:sch 2(A28, A29);
reconsider k = i - 1 as Nat by A27, NAT_1:20;
A41: i = k + 1 ;
then ( j <= k & k < i ) by A27, NAT_1:13;
then ((Ser f) . k) + (f . i) = ((Ser g) . k) + (g . i) by A40;
then (Ser f) . i = ((Ser g) . k) + (g . i) by A41, SUPINF_2:def 11;
hence (Ser f) . i = (Ser g) . i by A41, SUPINF_2:def 11; :: thesis: verum

end;

end;

end;

end;