let f be V184() Function of [:NAT,NAT:],ExtREAL; for n, m being Nat holds
( (Partial_Sums f) . ((n + 1),m) = ((Partial_Sums_in_cod2 f) . ((n + 1),m)) + ((Partial_Sums f) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m)) )
let n, m be Nat; ( (Partial_Sums f) . ((n + 1),m) = ((Partial_Sums_in_cod2 f) . ((n + 1),m)) + ((Partial_Sums f) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m)) )
reconsider g = - f as V183() Function of [:NAT,NAT:],ExtREAL ;
A2:
( dom (- (Partial_Sums_in_cod2 (Partial_Sums_in_cod1 g))) = [:NAT,NAT:] & dom (- (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g))) = [:NAT,NAT:] )
by FUNCT_2:def 1;
A4:
( dom (- (Partial_Sums_in_cod2 g)) = [:NAT,NAT:] & dom (- (Partial_Sums_in_cod1 g)) = [:NAT,NAT:] )
by FUNCT_2:def 1;
A5:
dom (- (Partial_Sums g)) = [:NAT,NAT:]
by FUNCT_2:def 1;
( n in NAT & m in NAT )
by ORDINAL1:def 12;
then A3:
( [(n + 1),m] in [:NAT,NAT:] & [n,m] in [:NAT,NAT:] & [n,(m + 1)] in [:NAT,NAT:] )
by ZFMISC_1:87;
A1: Partial_Sums f =
Partial_Sums_in_cod2 (Partial_Sums_in_cod1 (- g))
by Th2
.=
Partial_Sums_in_cod2 (- (Partial_Sums_in_cod1 g))
by Th42
.=
- (Partial_Sums g)
by Th42
;
thus (Partial_Sums f) . ((n + 1),m) =
- ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 g)) . ((n + 1),m))
by A1, A2, A3, MESFUNC1:def 7
.=
- (((Partial_Sums_in_cod2 g) . ((n + 1),m)) + ((Partial_Sums g) . (n,m)))
by Th47
.=
(- ((Partial_Sums_in_cod2 g) . ((n + 1),m))) - ((Partial_Sums g) . (n,m))
by XXREAL_3:25
.=
((- (Partial_Sums_in_cod2 g)) . ((n + 1),m)) + (- ((Partial_Sums g) . (n,m)))
by A3, A4, MESFUNC1:def 7
.=
((Partial_Sums_in_cod2 (- g)) . ((n + 1),m)) + (- ((Partial_Sums g) . (n,m)))
by Th42
.=
((Partial_Sums_in_cod2 f) . ((n + 1),m)) + (- ((Partial_Sums g) . (n,m)))
by Th2
.=
((Partial_Sums_in_cod2 f) . ((n + 1),m)) + ((Partial_Sums f) . (n,m))
by A1, A3, A5, MESFUNC1:def 7
; (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m))
thus (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) =
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 (- g))) . (n,(m + 1))
by Th2
.=
(Partial_Sums_in_cod1 (- (Partial_Sums_in_cod2 g))) . (n,(m + 1))
by Th42
.=
(- (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g))) . (n,(m + 1))
by Th42
.=
- ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g)) . (n,(m + 1)))
by A3, A2, MESFUNC1:def 7
.=
- (((Partial_Sums_in_cod1 g) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g)) . (n,m)))
by Th47
.=
(- ((Partial_Sums_in_cod1 g) . (n,(m + 1)))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g)) . (n,m))
by XXREAL_3:25
.=
((- (Partial_Sums_in_cod1 g)) . (n,(m + 1))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g)) . (n,m))
by A4, A3, MESFUNC1:def 7
.=
((- (Partial_Sums_in_cod1 g)) . (n,(m + 1))) + ((- (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g))) . (n,m))
by A3, A2, MESFUNC1:def 7
.=
((Partial_Sums_in_cod1 (- g)) . (n,(m + 1))) + ((- (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g))) . (n,m))
by Th42
.=
((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((- (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 g))) . (n,m))
by Th2
.=
((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (- (Partial_Sums_in_cod2 g))) . (n,m))
by Th42
.=
((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 (- g))) . (n,m))
by Th42
.=
((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m))
by Th2
; verum