let f1 be without-infty ExtREAL_sequence; for f2 being without+infty ExtREAL_sequence holds
( Partial_Sums (f1 - f2) = (Partial_Sums f1) - (Partial_Sums f2) & Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1) )
let f2 be without+infty ExtREAL_sequence; ( Partial_Sums (f1 - f2) = (Partial_Sums f1) - (Partial_Sums f2) & Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1) )
set P1 = Partial_Sums f1;
set P2 = Partial_Sums f2;
set P12 = Partial_Sums (f1 - f2);
set P21 = Partial_Sums (f2 - f1);
defpred S1[ Nat] means (Partial_Sums (f1 - f2)) . $1 = ((Partial_Sums f1) . $1) - ((Partial_Sums f2) . $1);
(Partial_Sums (f1 - f2)) . 0 = (f1 - f2) . 0
by MESFUNC9:def 1;
then
(Partial_Sums (f1 - f2)) . 0 = (f1 . 0) - (f2 . 0)
by DBLSEQ_3:7;
then
(Partial_Sums (f1 - f2)) . 0 = ((Partial_Sums f1) . 0) - (f2 . 0)
by MESFUNC9:def 1;
then A1:
S1[ 0 ]
by MESFUNC9:def 1;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
A4:
(
(Partial_Sums f1) . k <> -infty &
(Partial_Sums f2) . k <> +infty &
f1 . (k + 1) <> -infty &
f2 . (k + 1) <> +infty &
(f1 - f2) . (k + 1) <> -infty &
(Partial_Sums f2) . (k + 1) <> +infty )
by MESFUNC5:def 5, MESFUNC5:def 6;
then A5:
(
((Partial_Sums f2) . k) + (f2 . (k + 1)) <> +infty &
- (f1 . (k + 1)) <> +infty &
- ((Partial_Sums f2) . (k + 1)) <> -infty )
by XXREAL_3:16, XXREAL_3:23;
(Partial_Sums (f1 - f2)) . (k + 1) =
((Partial_Sums (f1 - f2)) . k) + ((f1 - f2) . (k + 1))
by MESFUNC9:def 1
.=
((Partial_Sums f1) . k) - (((Partial_Sums f2) . k) - ((f1 - f2) . (k + 1)))
by A3, A4, XXREAL_3:32
.=
((Partial_Sums f1) . k) - (((Partial_Sums f2) . k) - ((f1 . (k + 1)) - (f2 . (k + 1))))
by DBLSEQ_3:7
.=
((Partial_Sums f1) . k) - ((((Partial_Sums f2) . k) - (f1 . (k + 1))) + (f2 . (k + 1)))
by A4, XXREAL_3:32
.=
((Partial_Sums f1) . k) - (((- (f1 . (k + 1))) + ((Partial_Sums f2) . k)) + (f2 . (k + 1)))
by XXREAL_3:def 4
.=
((Partial_Sums f1) . k) - ((- (f1 . (k + 1))) + (((Partial_Sums f2) . k) + (f2 . (k + 1))))
by A4, A5, XXREAL_3:29
.=
((Partial_Sums f1) . k) - ((- (f1 . (k + 1))) + ((Partial_Sums f2) . (k + 1)))
by MESFUNC9:def 1
.=
((Partial_Sums f1) . k) - (((Partial_Sums f2) . (k + 1)) - (f1 . (k + 1)))
by XXREAL_3:def 4
.=
(((Partial_Sums f1) . k) - ((Partial_Sums f2) . (k + 1))) + (f1 . (k + 1))
by A4, XXREAL_3:32
.=
(((Partial_Sums f1) . k) + (- ((Partial_Sums f2) . (k + 1)))) + (f1 . (k + 1))
by XXREAL_3:def 4
.=
(((Partial_Sums f1) . k) + (f1 . (k + 1))) + (- ((Partial_Sums f2) . (k + 1)))
by A4, A5, XXREAL_3:29
.=
((Partial_Sums f1) . (k + 1)) + (- ((Partial_Sums f2) . (k + 1)))
by MESFUNC9:def 1
;
hence
S1[
k + 1]
by XXREAL_3:def 4;
verum
end;
A6:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
for k being Element of NAT holds (Partial_Sums (f1 - f2)) . k = ((Partial_Sums f1) - (Partial_Sums f2)) . k
hence
Partial_Sums (f1 - f2) = (Partial_Sums f1) - (Partial_Sums f2)
by FUNCT_2:63; Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1)
defpred S2[ Nat] means (Partial_Sums (f2 - f1)) . $1 = ((Partial_Sums f2) . $1) - ((Partial_Sums f1) . $1);
(Partial_Sums (f2 - f1)) . 0 =
(f2 - f1) . 0
by MESFUNC9:def 1
.=
(f2 . 0) - (f1 . 0)
by DBLSEQ_3:7
.=
((Partial_Sums f2) . 0) - (f1 . 0)
by MESFUNC9:def 1
;
then A7:
S2[ 0 ]
by MESFUNC9:def 1;
A8:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A9:
S2[
k]
;
S2[k + 1]
A10:
(
(Partial_Sums f2) . k <> +infty &
(Partial_Sums f1) . k <> -infty &
f2 . (k + 1) <> +infty &
f1 . (k + 1) <> -infty &
(f2 - f1) . (k + 1) <> +infty &
(Partial_Sums f1) . (k + 1) <> -infty )
by MESFUNC5:def 5, MESFUNC5:def 6;
then A11:
(
((Partial_Sums f1) . k) + (f1 . (k + 1)) <> -infty &
- (f2 . (k + 1)) <> -infty &
- ((Partial_Sums f1) . (k + 1)) <> +infty )
by XXREAL_3:17, XXREAL_3:23;
(Partial_Sums (f2 - f1)) . (k + 1) =
((Partial_Sums (f2 - f1)) . k) + ((f2 - f1) . (k + 1))
by MESFUNC9:def 1
.=
((Partial_Sums f2) . k) - (((Partial_Sums f1) . k) - ((f2 - f1) . (k + 1)))
by A9, A10, XXREAL_3:32
.=
((Partial_Sums f2) . k) - (((Partial_Sums f1) . k) - ((f2 . (k + 1)) - (f1 . (k + 1))))
by DBLSEQ_3:7
.=
((Partial_Sums f2) . k) - ((((Partial_Sums f1) . k) - (f2 . (k + 1))) + (f1 . (k + 1)))
by A10, XXREAL_3:32
.=
((Partial_Sums f2) . k) - (((- (f2 . (k + 1))) + ((Partial_Sums f1) . k)) + (f1 . (k + 1)))
by XXREAL_3:def 4
.=
((Partial_Sums f2) . k) - ((- (f2 . (k + 1))) + (((Partial_Sums f1) . k) + (f1 . (k + 1))))
by A10, A11, XXREAL_3:29
.=
((Partial_Sums f2) . k) - ((- (f2 . (k + 1))) + ((Partial_Sums f1) . (k + 1)))
by MESFUNC9:def 1
.=
((Partial_Sums f2) . k) - (((Partial_Sums f1) . (k + 1)) - (f2 . (k + 1)))
by XXREAL_3:def 4
.=
(((Partial_Sums f2) . k) - ((Partial_Sums f1) . (k + 1))) + (f2 . (k + 1))
by A10, XXREAL_3:32
.=
(((Partial_Sums f2) . k) + (- ((Partial_Sums f1) . (k + 1)))) + (f2 . (k + 1))
by XXREAL_3:def 4
.=
(((Partial_Sums f2) . k) + (f2 . (k + 1))) + (- ((Partial_Sums f1) . (k + 1)))
by A10, A11, XXREAL_3:29
.=
((Partial_Sums f2) . (k + 1)) + (- ((Partial_Sums f1) . (k + 1)))
by MESFUNC9:def 1
;
hence
S2[
k + 1]
by XXREAL_3:def 4;
verum
end;
A12:
for k being Nat holds S2[k]
from NAT_1:sch 2(A7, A8);
for k being Element of NAT holds (Partial_Sums (f2 - f1)) . k = ((Partial_Sums f2) - (Partial_Sums f1)) . k
hence
Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1)
by FUNCT_2:63; verum