let X be set ; :: thesis: for S being Field_Subset of X
for M being Measure of S
for F being Sep_Sequence of S
for n being Nat holds
( union (rng (F | (Segm (n + 1)))) in S & (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) )
let S be Field_Subset of X; :: thesis: for M being Measure of S
for F being Sep_Sequence of S
for n being Nat holds
( union (rng (F | (Segm (n + 1)))) in S & (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) )
let M be Measure of S; :: thesis: for F being Sep_Sequence of S
for n being Nat holds
( union (rng (F | (Segm (n + 1)))) in S & (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) )
let F be Sep_Sequence of S; :: thesis: for n being Nat holds
( union (rng (F | (Segm (n + 1)))) in S & (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) )
let n be Nat; :: thesis: ( union (rng (F | (Segm (n + 1)))) in S & (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) )
A2: rng (F | (Segm (0 + 1))) = (rng (F | (Segm 0))) \/ {(F . 0)} by Th57
.= {(F . 0)} ;
then A2a: union (rng (F | (Segm (0 + 1)))) = F . 0 by ZFMISC_1:25;
defpred S₁[ Nat] means union (rng (F | (Segm ($1 + 1)))) in S;
A14: S₁[ 0 ] by A2a;
A15: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A16: S₁[k] ; :: thesis: S₁[k + 1]
union (rng (F | (Segm ((k + 1) + 1)))) = union ((rng (F | (Segm (k + 1)))) \/ {(F . (k + 1))}) by Th57
.= (union (rng (F | (Segm (k + 1))))) \/ (union {(F . (k + 1))}) by ZFMISC_1:78
.= (union (rng (F | (Segm (k + 1))))) \/ (F . (k + 1)) by ZFMISC_1:25 ;
hence union (rng (F | (Segm ((k + 1) + 1)))) in S by A16, PROB_1:3; :: thesis: verum

end;

P1: for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A15);
hence union (rng (F | (Segm (n + 1)))) in S ; :: thesis: (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1)))))
defpred S₂[ Nat] means (Partial_Sums (M * F)) . $1 = M . (union (rng (F | (Segm ($1 + 1)))));
A1: (Partial_Sums (M * F)) . 0 = (M * F) . 0 by MESFUNC9:def 1
.= M . (F . 0) by FUNCT_2:15 ;
A3: S₂[ 0 ] by A1, A2, ZFMISC_1:25;
A4: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A5: S₂[n] ; :: thesis: S₂[n + 1]
A6: (Partial_Sums (M * F)) . (n + 1) = ((Partial_Sums (M * F)) . n) + ((M * F) . (n + 1)) by MESFUNC9:def 1
.= (M . (union (rng (F | (Segm (n + 1)))))) + (M . (F . (n + 1))) by A5, FUNCT_2:15 ;

A13: now :: thesis: for x being object holds not x in (union (rng (F | (Segm (n + 1))))) /\ (F . (n + 1))

assume ex x being object st x in (union (rng (F | (Segm (n + 1))))) /\ (F . (n + 1)) ; :: thesis: contradiction
then consider x being object such that
A7: x in (union (rng (F | (Segm (n + 1))))) /\ (F . (n + 1)) ;
A8: ( x in union (rng (F | (Segm (n + 1)))) & x in F . (n + 1) ) by A7, XBOOLE_0:def 4;
then consider A being set such that
A9: ( x in A & A in rng (F | (Segm (n + 1))) ) by TARSKI:def 4;
consider k being object such that
A10: ( k in dom (F | (Segm (n + 1))) & A = (F | (Segm (n + 1))) . k ) by A9, FUNCT_1:def 3;
reconsider k = k as Nat by A10;
A11: k < n + 1 by A10, RELAT_1:57, NAT_1:44;
A = F . k by A10, FUNCT_1:47;
then x in (F . k) /\ (F . (n + 1)) by A8, A9, XBOOLE_0:def 4;
hence contradiction by A11, PROB_2:def 2, XBOOLE_0:4; :: thesis: verum

end;

union (rng (F | (Segm (n + 1)))) in S by P1;
then (M . (union (rng (F | (Segm (n + 1)))))) + (M . (F . (n + 1))) = M . ((union (rng (F | (Segm (n + 1))))) \/ (F . (n + 1))) by A13, XBOOLE_0:4, MEASURE1:def 8
.= M . ((union (rng (F | (Segm (n + 1))))) \/ (union {(F . (n + 1))})) by ZFMISC_1:25
.= M . (union ((rng (F | (Segm (n + 1)))) \/ {(F . (n + 1))})) by ZFMISC_1:78
.= M . (union (rng (F | (Segm ((n + 1) + 1))))) by Th57 ;
hence S₂[n + 1] by A6; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A3, A4);
hence (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) ; :: thesis: verum