let X be set ; :: thesis:
let S be semialgebra_of_sets of X; :: thesis:
let P be pre-Measure of S; :: thesis:
let M be Measure of (Field_generated_by S); :: thesis:
assume A1: for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F) ; :: thesis:

let FSets be Sep_Sequence of (Field_generated_by S); :: thesis:
assume B0: union (rng FSets) in Field_generated_by S ; :: thesis:
then union (rng FSets) in DisUnion S by SRINGS_3:22;
then consider A being Subset of X such that
B1: ( A = union (rng FSets) & ex F being disjoint_valued FinSequence of S st A = Union F ) ;
consider D being disjoint_valued FinSequence of S such that
B2: A = Union D by B1;
set Z = { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } ;
reconsider Y = proj2 { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } as FinSequenceSet of S by Th51;
E4: Y is with_non-empty_elements by Th51;

suppose rng FSets is with_non-empty_element ; :: thesis:

then consider a being non empty set such that
E6: a in rng FSets ;
ex E being FinSequence of S st
( E in Y & Union E = a ) by E6, Th51;
then reconsider Y = Y as non empty with_non-empty_element FinSequenceSet of S by E4;
defpred S₁[ Element of NAT , object ] means [$1,$2] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } ;
F2: for n being Element of NAT ex y being Element of Y st S₁[n,y]

proof

let n be Element of NAT ; :: thesis:
FSets . n in Field_generated_by S ;
then FSets . n in DisUnion S by SRINGS_3:22;
then consider A being Subset of X such that
F3: ( FSets . n = A & ex F being disjoint_valued FinSequence of S st A = Union F ) ;
consider F being disjoint_valued FinSequence of S such that
F4: A = Union F by F3;

per cases ;

suppose F5: FSets . n = {} ; :: thesis:

F6: rng <*{}*> = {{}} by FINSEQ_1:38;
{} in S by SETFAM_1:def 8;
then reconsider E = <*{}*> as disjoint_valued FinSequence of S by F6, ZFMISC_1:31, FINSEQ_1:def 4;
union (rng E) = {} by F6, ZFMISC_1:25;
then Union E = {} by CARD_3:def 4;
then F7: [n,E] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } by F5;
then E in Y by XTUPLE_0:def 13;
hence ex y being Element of Y st S₁[n,y] by F7; :: thesis:

end;

suppose FSets . n <> {} ; :: thesis:

then F8: [n,F] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } by F4, F3;
then F in Y by XTUPLE_0:def 13;
hence ex y being Element of Y st S₁[n,y] by F8; :: thesis:

end;

consider s being Function of NAT,Y such that
F9: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(F2);

now :: thesis:

let n be object ; :: thesis:
assume n in dom s ; :: thesis:
then reconsider n1 = n as Element of NAT ;
[n1,(s . n1)] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } by F9;
then F11: ex m being Nat ex E being disjoint_valued FinSequence of S st
( [n1,(s . n1)] = [m,E] & Union E = FSets . m & ( FSets . m = {} implies E = <*{}*> ) ) ;

now :: thesis:

assume F15: s . n = {} ; :: thesis:
then union (rng (s . n1)) = {} by ZFMISC_1:2;
then Union (s . n1) = {} by CARD_3:def 4;
hence contradiction by F11, F15, XTUPLE_0:1; :: thesis:

end;

hence not s . n is empty ; :: thesis:

end;

then reconsider s = s as non-empty sequence of Y by FUNCT_1:def 9;
reconsider G = joined_seq s as sequence of S ;

now :: thesis:

let x, y be object ; :: thesis:
assume F16: x <> y ; :: thesis:

per cases ;

suppose ( not x in NAT or not y in NAT ) ; :: thesis:

then ( not x in dom G or not y in dom G ) ;
then ( G . x = {} or G . y = {} ) by FUNCT_1:def 2;
hence G . x misses G . y by XBOOLE_1:65; :: thesis:

end;

suppose ( x in NAT & y in NAT ) ; :: thesis:

then reconsider n1 = x, n2 = y as Element of NAT ;
consider k1, m1 being Nat such that
F17: ( m1 in dom (s . k1) & ((((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1) - 1 = n1 & G . n1 = (s . k1) . m1 ) by Def4;
consider k2, m2 being Nat such that
F18: ( m2 in dom (s . k2) & ((((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2) - 1 = n2 & G . n2 = (s . k2) . m2 ) by Def4;
( k1 is Element of NAT & k2 is Element of NAT ) by ORDINAL1:def 12;
then F21: ( [k1,(s . k1)] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } & [k2,(s . k2)] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } ) by F9;
then consider i1 being Nat, E1 being disjoint_valued FinSequence of S such that
F22: ( [k1,(s . k1)] = [i1,E1] & Union E1 = FSets . i1 & ( FSets . i1 = {} implies E1 = <*{}*> ) ) ;
consider i2 being Nat, E2 being disjoint_valued FinSequence of S such that
F23: ( [k2,(s . k2)] = [i2,E2] & Union E2 = FSets . i2 & ( FSets . i2 = {} implies E2 = <*{}*> ) ) by F21;
F24: ( k1 = i1 & s . k1 = E1 & k2 = i2 & s . k2 = E2 ) by F22, F23, XTUPLE_0:1;

now :: thesis:

assume k1 <> k2 ; :: thesis:
then FSets . i1 misses FSets . i2 by F24, PROB_2:def 2;
then union (rng (s . k1)) misses Union (s . k2) by F22, F23, F24, CARD_3:def 4;
then F25: union (rng (s . k1)) misses union (rng (s . k2)) by CARD_3:def 4;
( G . n1 c= union (rng (s . k1)) & G . n2 c= union (rng (s . k2)) ) by F17, F18, FUNCT_1:3, ZFMISC_1:74;
hence G . n1 misses G . n2 by F25, XBOOLE_1:64; :: thesis:

end;

hence G . x misses G . y by F16, F17, F18, F24, PROB_2:def 2; :: thesis:

end;

then reconsider G = G as disjoint_valued sequence of S by PROB_2:def 2;

now :: thesis:

let x be object ; :: thesis:
assume x in Union FSets ; :: thesis:
then x in union (rng FSets) by CARD_3:def 4;
then consider A being set such that
G1: ( x in A & A in rng FSets ) by TARSKI:def 4;
consider n being Element of NAT such that
G2: A = FSets . n by G1, FUNCT_2:113;
[n,(s . n)] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } by F9;
then consider n2 being Nat, E2 being disjoint_valued FinSequence of S such that
G6: ( [n,(s . n)] = [n2,E2] & Union E2 = FSets . n2 & ( FSets . n2 = {} implies E2 = <*{}*> ) ) ;
( n = n2 & s . n = E2 ) by G6, XTUPLE_0:1;
then x in union (rng (s . n)) by G1, G2, G6, CARD_3:def 4;
then consider A2 being set such that
G8: ( x in A2 & A2 in rng (s . n) ) by TARSKI:def 4;
consider m being object such that
G9: ( m in dom (s . n) & A2 = (s . n) . m ) by G8, FUNCT_1:def 3;
reconsider m = m as Nat by G9;
consider N being Nat such that
G10: ( N = ((((Partial_Sums (Length s)) . n) - (len (s . n))) + m) - 1 & G . N = (s . n) . m ) by G9, Th13;
A2 in rng G by FUNCT_2:4, G9, G10, ORDINAL1:def 12;
then x in union (rng G) by G8, TARSKI:def 4;
hence x in Union G by CARD_3:def 4; :: thesis:

end;

then T0: Union FSets c= Union G by TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in Union G ; :: thesis:
then x in union (rng G) by CARD_3:def 4;
then consider A being set such that
G11: ( x in A & A in rng G ) by TARSKI:def 4;
consider n being Element of NAT such that
G12: A = G . n by G11, FUNCT_2:113;
consider k, m being Nat such that
G13: ( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & G . n = (s . k) . m ) by Def4;
k is Element of NAT by ORDINAL1:def 12;
then [k,(s . k)] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } by F9;
then consider k2 being Nat, E being disjoint_valued FinSequence of S such that
G14: ( [k,(s . k)] = [k2,E] & Union E = FSets . k2 & ( FSets . k2 = {} implies E = <*{}*> ) ) ;
G15: ( k = k2 & s . k = E ) by G14, XTUPLE_0:1;
( x in (s . k) . m & (s . k) . m in rng (s . k) ) by G11, G12, G13, FUNCT_1:3;
then x in union (rng (s . k)) by TARSKI:def 4;
then G16: x in FSets . k2 by G14, G15, CARD_3:def 4;
FSets . k2 in rng FSets by FUNCT_2:4, ORDINAL1:def 12;
then x in union (rng FSets) by G16, TARSKI:def 4;
hence x in Union FSets by CARD_3:def 4; :: thesis:

end;

then Union G c= Union FSets by TARSKI:def 3;
then T1: Union FSets = Union G by T0, XBOOLE_0:def 10;
defpred S₂[ Nat, Nat, object ] means ( ( $1 + 1 <= len D implies $3 = (D . ($1 + 1)) /\ (G . $2) ) & ( $1 + 1 > len D implies $3 = {} ) );
D0: for i, j being Element of NAT ex z being Element of S st S₂[i,j,z]

proof

let i, j be Element of NAT ; :: thesis:

per cases ;

suppose D1: i + 1 <= len D ; :: thesis:

then i + 1 in dom D by NAT_1:11, FINSEQ_3:25;
then D . (i + 1) in rng D by FUNCT_1:3;
then (D . (i + 1)) /\ (G . j) in S by FINSUB_1:def 2;
hence ex z being Element of S st S₂[i,j,z] by D1; :: thesis:

end;

suppose D4: i + 1 > len D ; :: thesis:

{} in S by SETFAM_1:def 8;
hence ex z being Element of S st S₂[i,j,z] by D4; :: thesis:

end;

consider LG being Function of [:NAT,NAT:],S such that
D5: for i, j being Element of NAT holds S₂[i,j,LG . (i,j)] from BINOP_1:sch 3(D0);
D5a: for i, j being Nat holds
( ( i + 1 <= len D implies LG . (i,j) = (D . (i + 1)) /\ (G . j) ) & ( i + 1 > len D implies LG . (i,j) = {} ) )

proof

let i, j be Nat; :: thesis:
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def 12;

DD5: now :: thesis:

assume i + 1 <= len D ; :: thesis:
then LG . (i1,j1) = (D . (i + 1)) /\ (G . j) by D5;
hence LG . (i,j) = (D . (i + 1)) /\ (G . j) ; :: thesis:

end;

now :: thesis:

assume i + 1 > len D ; :: thesis:
then LG . (i1,j1) = {} by D5;
hence LG . (i,j) = {} ; :: thesis:

end;

hence ( ( i + 1 <= len D implies LG . (i,j) = (D . (i + 1)) /\ (G . j) ) & ( i + 1 > len D implies LG . (i,j) = {} ) ) by DD5; :: thesis:

end;

Union FSets = union (rng FSets) by CARD_3:def 4;
then X2: M . (Union FSets) = Sum (P * D) by A1, B0, B1, B2;
consider SumPD being sequence of ExtREAL such that
X3: ( Sum (P * D) = SumPD . (len (P * D)) & SumPD . 0 = 0. & ( for i being Nat st i < len (P * D) holds
SumPD . (i + 1) = (SumPD . i) + ((P * D) . (i + 1)) ) ) by EXTREAL1:def 2;
X4: for i being Element of NAT st i < len D holds
D . (i + 1) = Union (ProjMap1 (LG,i))

proof

let i be Element of NAT ; :: thesis:
assume X40: i < len D ; :: thesis:
then ( 1 <= i + 1 & i + 1 <= len D ) by NAT_1:11, NAT_1:13;
then i + 1 in dom D by FINSEQ_3:25;
then X41: D . (i + 1) in rng D by FUNCT_1:3;

now :: thesis:

let x be object ; :: thesis:
assume X44: x in D . (i + 1) ; :: thesis:
then x in union (rng D) by X41, TARSKI:def 4;
then x in Union D by CARD_3:def 4;
then x in Union G by B1, B2, T1, CARD_3:def 4;
then x in union (rng G) by CARD_3:def 4;
then consider Gx being set such that
X42: ( x in Gx & Gx in rng G ) by TARSKI:def 4;
consider j being Element of NAT such that
X43: Gx = G . j by X42, FUNCT_2:113;
X46: dom (ProjMap1 (LG,i)) = NAT by FUNCT_2:def 1;
X45: x in (D . (i + 1)) /\ (G . j) by X44, X42, X43, XBOOLE_0:def 4;
( i + 1 <= len D implies LG . (i,j) = (D . (i + 1)) /\ (G . j) ) by D5;
then X47: x in (ProjMap1 (LG,i)) . j by X40, NAT_1:13, X45, MESFUNC9:def 6;
(ProjMap1 (LG,i)) . j in rng (ProjMap1 (LG,i)) by X46, FUNCT_1:3;
then x in union (rng (ProjMap1 (LG,i))) by X47, TARSKI:def 4;
hence x in Union (ProjMap1 (LG,i)) by CARD_3:def 4; :: thesis:

end;

then X48: D . (i + 1) c= Union (ProjMap1 (LG,i)) by TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in Union (ProjMap1 (LG,i)) ; :: thesis:
then x in union (rng (ProjMap1 (LG,i))) by CARD_3:def 4;
then consider Px being set such that
X50: ( x in Px & Px in rng (ProjMap1 (LG,i)) ) by TARSKI:def 4;
consider j being Element of NAT such that
X51: Px = (ProjMap1 (LG,i)) . j by X50, FUNCT_2:113;
(ProjMap1 (LG,i)) . j = LG . (i,j) by MESFUNC9:def 6;
then x in (D . (i + 1)) /\ (G . j) by X50, X51, D5;
hence x in D . (i + 1) by XBOOLE_0:def 4; :: thesis:

end;

then Union (ProjMap1 (LG,i)) c= D . (i + 1) by TARSKI:def 3;
hence D . (i + 1) = Union (ProjMap1 (LG,i)) by X48, XBOOLE_0:def 10; :: thesis:

end;

X5: for i being Element of NAT st i < len D holds
(P * D) . (i + 1) <= (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . i

proof

let i be Element of NAT ; :: thesis:
assume X50: i < len D ; :: thesis:
then X50a: ( 1 <= i + 1 & i + 1 <= len D ) by NAT_1:11, NAT_1:13;
then X51: i + 1 in dom D by FINSEQ_3:25;
then X52: D . (i + 1) in rng D by FUNCT_1:3;

now :: thesis:

let x, y be object ; :: thesis:
assume V1: x <> y ; :: thesis:

per cases ;

suppose ( not x in dom (ProjMap1 (LG,i)) or not y in dom (ProjMap1 (LG,i)) ) ; :: thesis:

then ( (ProjMap1 (LG,i)) . x = {} or (ProjMap1 (LG,i)) . y = {} ) by FUNCT_1:def 2;
hence (ProjMap1 (LG,i)) . x misses (ProjMap1 (LG,i)) . y by XBOOLE_1:65; :: thesis:

end;

suppose ( x in dom (ProjMap1 (LG,i)) & y in dom (ProjMap1 (LG,i)) ) ; :: thesis:

then reconsider x1 = x, y1 = y as Element of NAT ;
( (ProjMap1 (LG,i)) . x = LG . (i,x1) & (ProjMap1 (LG,i)) . y = LG . (i,y1) ) by MESFUNC9:def 6;
then ( (ProjMap1 (LG,i)) . x = (D . (i + 1)) /\ (G . x1) & (ProjMap1 (LG,i)) . y = (D . (i + 1)) /\ (G . y1) ) by X50a, D5;
hence (ProjMap1 (LG,i)) . x misses (ProjMap1 (LG,i)) . y by V1, PROB_2:def 2, XBOOLE_1:76; :: thesis:

end;

then X53: ProjMap1 (LG,i) is disjoint_valued Function of NAT,S by PROB_2:def 2;
X54: D . (i + 1) = Union (ProjMap1 (LG,i)) by X4, X50;
X55: (P * D) . (i + 1) = P . (D . (i + 1)) by X51, FUNCT_1:13
.= P . (Union (ProjMap1 (LG,i))) by X4, X50 ;

X56: now :: thesis:

let k be Element of NAT ; :: thesis:
P . (LG . (i,k)) = (P * LG) . (i,k) by ZFMISC_1:87, FUNCT_2:15;
then (ProjMap1 ((P * LG),i)) . k = P . (LG . (i,k)) by MESFUNC9:def 6
.= P . ((ProjMap1 (LG,i)) . k) by MESFUNC9:def 6 ;
hence (P * (ProjMap1 (LG,i))) . k = (ProjMap1 ((P * LG),i)) . k by FUNCT_2:15; :: thesis:

end;

SUM (P * (ProjMap1 (LG,i))) = Sum (P * (ProjMap1 (LG,i))) by MEASURE8:2
.= lim (Partial_Sums (P * (ProjMap1 (LG,i)))) by MESFUNC9:def 3
.= lim (Partial_Sums (ProjMap1 ((P * LG),i))) by X56, FUNCT_2:def 8
.= lim (ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),i)) by DBLSEQ_3:53
.= (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . i by DBLSEQ_3:def 13 ;
hence (P * D) . (i + 1) <= (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . i by X55, X52, X53, X54, Def8; :: thesis:

end;

defpred S₃[ Nat] means ( $1 < len (P * D) implies SumPD . ($1 + 1) <= (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . $1 );
rng D c= S ;
then rng D c= dom P by FUNCT_2:def 1;
then dom (P * D) = dom D by RELAT_1:27;
then X71: len (P * D) = len D by FINSEQ_3:29;

now :: thesis:

assume X60: 0 < len (P * D) ; :: thesis:
then X61: (P * D) . (0 + 1) <= (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . 0 by X5, X71;
SumPD . (0 + 1) = (SumPD . 0) + ((P * D) . (0 + 1)) by X60, X3;
then SumPD . (0 + 1) = (P * D) . 1 by X3, XXREAL_3:4;
hence SumPD . (0 + 1) <= (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . 0 by X61, MESFUNC9:def 1; :: thesis:

end;

then X62: S₃[ 0 ] ;
X63: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
assume X64: S₃[k] ; :: thesis:
assume X65: k + 1 < len (P * D) ; :: thesis:
then X67: (P * D) . ((k + 1) + 1) <= (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . (k + 1) by X5, X71;
SumPD . ((k + 1) + 1) = (SumPD . (k + 1)) + ((P * D) . ((k + 1) + 1)) by X3, X65;
then SumPD . ((k + 1) + 1) <= ((Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . (k + 1)) by NAT_1:13, X67, X64, X65, XXREAL_3:36;
hence SumPD . ((k + 1) + 1) <= (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (k + 1) by MESFUNC9:def 1; :: thesis:

end;

X68: for k being Nat holds S₃[k] from NAT_1:sch 2(X62, X63);

XX70: now :: thesis:

assume D = {} ; :: thesis:
then union (rng D) = {} by ZFMISC_1:2;
then X69: union (rng FSets) = {} by B1, B2, CARD_3:def 4;
union {a} c= union (rng FSets) by E6, ZFMISC_1:31, ZFMISC_1:77;
hence contradiction by X69; :: thesis:

end;

then consider i1 being Nat such that
X70: len D = i1 + 1 by NAT_1:6;
reconsider i1 = i1 as Element of NAT by ORDINAL1:def 12;
i1 < len D by X70, NAT_1:13;
then X72: Sum (P * D) <= (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . i1 by X70, X71, X68, X3;
X73: len (P * D) >= i1 by X70, X71, NAT_1:11;
W3: Partial_Sums_in_cod2 (P * LG) is convergent_in_cod2 by DBLSEQ_3:66;
then X80: lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)) is V224() by DBLSEQ_3:65;
then X74: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . i1 <= (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) by X73, RINFSUP2:7, MESFUNC9:16;
(Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) = (lim_in_cod2 (Partial_Sums (P * LG))) . (len (P * D))

proof

per cases ) . (len (P * D)) = +infty or (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) <> +infty ) ;

suppose X75: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) = +infty ; :: thesis:

then ex k being Element of NAT st
( k <= len (P * D) & ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),k) is convergent_to_+infty ) by DBLSEQ_3:74;
then lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 (P * LG))),(len (P * D)))) = +infty by DBLSEQ_3:77;
then lim (ProjMap1 ((Partial_Sums (P * LG)),(len (P * D)))) = +infty by DBLSEQ_3:def 16;
hence (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) = (lim_in_cod2 (Partial_Sums (P * LG))) . (len (P * D)) by X75, DBLSEQ_3:def 13; :: thesis:

end;

suppose (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) <> +infty ; :: thesis:

then X81: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) < +infty by XXREAL_0:4;
for m being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),m) is convergent_to_finite_number

proof

let m be Element of NAT ; :: thesis:
W5: ( ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),m) is convergent_to_+infty or ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),m) is convergent_to_finite_number or ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),m) is convergent_to_-infty ) by W3, DBLSEQ_3:def 11, MESFUNC5:def 11;

per cases ;

suppose m <= len (P * D) ; :: thesis:

end;

suppose m > len (P * D) ; :: thesis:

then consider j being Nat such that
W7: m = (len (P * D)) + j by NAT_1:10;
defpred S₄[ Nat] means (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . ((len (P * D)) + $1) = (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D));
W8: S₄[ 0 ] ;
W9: for i being Nat st S₄[i] holds
S₄[i + 1]

proof

let i be Nat; :: thesis:
assume W12: S₄[i] ; :: thesis:
W13: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (((len (P * D)) + i) + 1) = ((Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D))) + ((lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . (((len (P * D)) + i) + 1)) by W12, MESFUNC9:def 1;
for s being Nat holds (ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),(((len (P * D)) + i) + 1))) . s = 0

proof

let s be Nat; :: thesis:
reconsider s1 = s as Element of NAT by ORDINAL1:def 12;
W15: (ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),(((len (P * D)) + i) + 1))) . s1 = (Partial_Sums_in_cod2 (P * LG)) . ((((len (P * D)) + i) + 1),s) by MESFUNC9:def 6;
P0: for k, j being Nat holds (P * LG) . ((((len (P * D)) + k) + 1),j) = 0

proof

let k, j be Nat; :: thesis:
reconsider k1 = k, j1 = j as Element of NAT by ORDINAL1:def 12;
((len D) + k) + 1 >= len D by NAT_1:11, NAT_1:12;
then P1: (((len D) + k1) + 1) + 1 > len D by NAT_1:13;
[(((len (P * D)) + k1) + 1),j1] in [:NAT,NAT:] by ZFMISC_1:87;
then [(((len (P * D)) + k1) + 1),j1] in dom LG by FUNCT_2:def 1;
then (P * LG) . ((((len (P * D)) + k) + 1),j) = P . (LG . ((((len D) + k1) + 1),j1)) by X71, FUNCT_1:13;
then (P * LG) . ((((len (P * D)) + k) + 1),j) = P . {} by D5, P1;
hence (P * LG) . ((((len (P * D)) + k) + 1),j) = 0 by VALUED_0:def 19; :: thesis:

end;

defpred S₅[ Nat] means (Partial_Sums_in_cod2 (P * LG)) . ((((len (P * D)) + i) + 1),$1) = 0 ;
(Partial_Sums_in_cod2 (P * LG)) . ((((len (P * D)) + i) + 1),0) = (P * LG) . ((((len (P * D)) + i) + 1),0) by DBLSEQ_3:def 14;
then W16: S₅[ 0 ] by P0;
W17: for j being Nat st S₅[j] holds
S₅[j + 1]

proof

let j be Nat; :: thesis:
assume P2: S₅[j] ; :: thesis:
(Partial_Sums_in_cod2 (P * LG)) . ((((len (P * D)) + i) + 1),(j + 1)) = ((Partial_Sums_in_cod2 (P * LG)) . ((((len (P * D)) + i) + 1),j)) + ((P * LG) . ((((len (P * D)) + i) + 1),(j + 1))) by DBLSEQ_3:def 14
.= (P * LG) . ((((len (P * D)) + i) + 1),(j + 1)) by P2, XXREAL_3:4 ;
hence S₅[j + 1] by P0; :: thesis:

end;

for j being Nat holds S₅[j] from NAT_1:sch 2(W16, W17);
hence (ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),(((len (P * D)) + i) + 1))) . s = 0 by W15; :: thesis:

end;

then lim (ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),(((len (P * D)) + i) + 1))) = 0 by MESFUNC5:52;
then (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . (((len (P * D)) + i) + 1) = 0 by DBLSEQ_3:def 13;
hence S₄[i + 1] by W13, XXREAL_3:4; :: thesis:

end;

for i being Nat holds S₄[i] from NAT_1:sch 2(W8, W9);
then S₄[j] ;
then W10: (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . m <= (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) by W7, X80, DBLSEQ_3:4;
(lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . m > -infty by X80, SUPINF_2:51;
then (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG))) . m in REAL by W10, X81, XXREAL_0:14;
then lim (ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),m)) in REAL by DBLSEQ_3:def 13;
hence ProjMap1 ((Partial_Sums_in_cod2 (P * LG)),m) is convergent_to_finite_number by W5, MESFUNC5:def 12; :: thesis:

end;

then Partial_Sums (P * LG) is convergent_in_cod2_to_finite by DBLSEQ_3:def 10, DBLSEQ_3:81;
then (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) = lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 (P * LG))),(len (P * D)))) by DBLSEQ_3:82
.= lim (ProjMap1 ((Partial_Sums (P * LG)),(len (P * D)))) by DBLSEQ_3:def 16 ;
hence (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 (P * LG)))) . (len (P * D)) = (lim_in_cod2 (Partial_Sums (P * LG))) . (len (P * D)) by DBLSEQ_3:def 13; :: thesis:

end;

then X100: Sum (P * D) <= (lim_in_cod2 (Partial_Sums (P * LG))) . (len (P * D)) by X74, X72, XXREAL_0:2;
for j being Nat holds (Partial_Sums_in_cod1 (P * LG)) . ((len (P * D)),j) = (P * G) . j

proof

let j be Nat; :: thesis:
reconsider j1 = j as Element of NAT by ORDINAL1:def 12;
consider k, m being Nat such that
M0: ( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = j & G . j = (s . k) . m ) by Def4;
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
[k1,(s . k1)] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } by F9;
then consider k2 being Nat, Sk being disjoint_valued FinSequence of S such that
M1: ( [k1,(s . k1)] = [k2,Sk] & Union Sk = FSets . k2 & ( FSets . k2 = {} implies Sk = <*{}*> ) ) ;
M2: ( s . k = Sk & Union Sk = FSets . k & ( FSets . k = {} implies Sk = <*{}*> ) ) by M1, XTUPLE_0:1;
defpred S₄[ Nat, object ] means $2 = (D . $1) /\ (G . j);
M3: for k being Nat st k in Seg (len D) holds
ex x being Element of S st S₄[k,x]

proof

let k be Nat; :: thesis:
assume M5: k in Seg (len D) ; :: thesis:
then ( 1 <= k & k <= len D ) by FINSEQ_1:1;
then consider k1 being Nat such that
M4: k = k1 + 1 by NAT_1:6;
reconsider kk1 = k1 as Element of NAT by ORDINAL1:def 12;
LG . (kk1,j1) = (D . k) /\ (G . j) by M4, M5, D5, FINSEQ_1:1;
hence ex x being Element of S st S₄[k,x] ; :: thesis:

end;

consider Cj being FinSequence of S such that
M7: ( dom Cj = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S₄[k,Cj . k] ) ) from FINSEQ_1:sch 5(M3);
M7a: len Cj = len D by M7, FINSEQ_1:def 3;

now :: thesis:

let x, y be object ; :: thesis:
assume M61: x <> y ; :: thesis:

per cases ;

suppose M62: ( x in dom Cj & y in dom Cj ) ; :: thesis:

then reconsider x1 = x, y1 = y as Nat ;
( Cj . x = (D . x1) /\ (G . j) & Cj . y = (D . y1) /\ (G . j) ) by M7, M62;
hence Cj . x misses Cj . y by M61, PROB_2:def 2, XBOOLE_1:76; :: thesis:

end;

suppose ( not x in dom Cj or not y in dom Cj ) ; :: thesis:

then ( Cj . x = {} or Cj . y = {} ) by FUNCT_1:def 2;
hence Cj . x misses Cj . y by XBOOLE_1:65; :: thesis:

end;

then reconsider Cj = Cj as disjoint_valued FinSequence of S by PROB_2:def 2;

now :: thesis:

let x be object ; :: thesis:
assume x in Union Cj ; :: thesis:
then x in union (rng Cj) by CARD_3:def 4;
then consider V being set such that
M64: ( x in V & V in rng Cj ) by TARSKI:def 4;
consider y being object such that
M65: ( y in dom Cj & V = Cj . y ) by M64, FUNCT_1:def 3;
reconsider y = y as Nat by M65;
Cj . y = (D . y) /\ (G . j) by M65, M7;
hence x in G . j by M64, M65, XBOOLE_0:def 4; :: thesis:

end;

then M66: Union Cj c= G . j by TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume M67a: x in G . j ; :: thesis:
then ( x in Sk . m & Sk . m in rng Sk ) by M0, M2, FUNCT_1:3;
then x in union (rng Sk) by TARSKI:def 4;
then M67: x in FSets . k2 by M1, CARD_3:def 4;
dom FSets = NAT by FUNCT_2:def 1;
then FSets . k2 in rng FSets by FUNCT_1:3, ORDINAL1:def 12;
then x in union (rng FSets) by M67, TARSKI:def 4;
then x in union (rng D) by B1, B2, CARD_3:def 4;
then consider V being set such that
M68: ( x in V & V in rng D ) by TARSKI:def 4;
consider y being object such that
M69: ( y in dom D & V = D . y ) by M68, FUNCT_1:def 3;
reconsider y = y as Nat by M69;
M70: x in (D . y) /\ (G . j) by M67a, M68, M69, XBOOLE_0:def 4;
y in Seg (len D) by M69, FINSEQ_1:def 3;
then M71: x in Cj . y by M7, M70;
y in dom Cj by M69, FINSEQ_1:def 3, M7;
then Cj . y in rng Cj by FUNCT_1:3;
then x in union (rng Cj) by M71, TARSKI:def 4;
hence x in Union Cj by CARD_3:def 4; :: thesis:

end;

then G . j c= Union Cj by TARSKI:def 3;
then M6: Union Cj = G . j by M66, XBOOLE_0:def 10;
M6b: P . (G . j) = Sum (P * Cj) by M6, Def8;
j in NAT by ORDINAL1:def 12;
then j in dom G by FUNCT_2:def 1;
then M6a: (P * G) . j = Sum (P * Cj) by M6b, FUNCT_1:13;
consider SumPCj being sequence of ExtREAL such that
M8: ( Sum (P * Cj) = SumPCj . (len (P * Cj)) & SumPCj . 0 = 0. & ( for i being Nat st i < len (P * Cj) holds
SumPCj . (i + 1) = (SumPCj . i) + ((P * Cj) . (i + 1)) ) ) by EXTREAL1:def 2;
rng Cj c= S ;
then rng Cj c= dom P by FUNCT_2:def 1;
then N9: dom (P * Cj) = dom Cj by RELAT_1:27;
then M9: len (P * Cj) = len Cj by FINSEQ_3:29;
M13: for i being Nat st i < len D holds
(P * Cj) . (i + 1) = (P * LG) . (i,j)

proof

let i be Nat; :: thesis:
assume i < len D ; :: thesis:
then M11: ( 1 <= i + 1 & i + 1 <= len D ) by NAT_1:11, NAT_1:13;
then M12: i + 1 in Seg (len D) ;
(P * Cj) . (i + 1) = P . (Cj . (i + 1)) by M11, N9, M7a, FINSEQ_3:25, FUNCT_1:12;
then (P * Cj) . (i + 1) = P . ((D . (i + 1)) /\ (G . j)) by M7, M12;
then M10: (P * Cj) . (i + 1) = P . (LG . (i,j)) by M11, D5a;
( i in NAT & j in NAT ) by ORDINAL1:def 12;
then [i,j] in [:NAT,NAT:] by ZFMISC_1:87;
then [i,j] in dom LG by FUNCT_2:def 1;
hence (P * Cj) . (i + 1) = (P * LG) . (i,j) by M10, FUNCT_1:13; :: thesis:

end;

MM15: (len (P * D)) + 1 > len D by X71, NAT_1:13;
( len (P * D) in NAT & j in NAT ) by ORDINAL1:def 12;
then [(len (P * D)),j] in [:NAT,NAT:] by ZFMISC_1:87;
then [(len (P * D)),j] in dom LG by FUNCT_2:def 1;
then (P * LG) . ((len (P * D)),j) = P . (LG . ((len (P * D)),j)) by FUNCT_1:13;
then (P * LG) . ((len (P * D)),j) = P . {} by MM15, D5a;
then M15: (P * LG) . ((len (P * D)),j) = 0 by VALUED_0:def 19;
consider LENDM1 being Nat such that
M23: len D = LENDM1 + 1 by XX70, NAT_1:6;
M24: LENDM1 < len (P * D) by M23, X71, NAT_1:13;
defpred S₅[ Nat] means ( $1 < len (P * D) implies (Partial_Sums_in_cod1 (P * LG)) . ($1,j) = SumPCj . ($1 + 1) );
(Partial_Sums_in_cod1 (P * LG)) . (0,j) = (P * LG) . (0,j) by DBLSEQ_3:def 15;
then M17: (Partial_Sums_in_cod1 (P * LG)) . (0,j) = (P * Cj) . (0 + 1) by XX70, M13;
SumPCj . (0 + 1) = 0 + ((P * Cj) . (0 + 1)) by XX70, M7a, M9, M8;
then M18: S₅[ 0 ] by M17, XXREAL_3:4;
M22: for k being Nat st S₅[k] holds
S₅[k + 1]

proof

let k be Nat; :: thesis:
assume M19: S₅[k] ; :: thesis:
assume M20: k + 1 < len (P * D) ; :: thesis:
then (Partial_Sums_in_cod1 (P * LG)) . ((k + 1),j) = (SumPCj . (k + 1)) + ((P * LG) . ((k + 1),j)) by M19, NAT_1:13, DBLSEQ_3:def 15
.= (SumPCj . (k + 1)) + ((P * Cj) . ((k + 1) + 1)) by M20, M13, X71 ;
hence (Partial_Sums_in_cod1 (P * LG)) . ((k + 1),j) = SumPCj . ((k + 1) + 1) by M20, M9, M7a, M8, X71; :: thesis:

end;

for k being Nat holds S₅[k] from NAT_1:sch 2(M18, M22);
then (Partial_Sums_in_cod1 (P * LG)) . (LENDM1,j) = (P * G) . j by M6a, M8, M24, M23, M7a, M9;
then (Partial_Sums_in_cod1 (P * LG)) . ((len (P * D)),j) = ((P * G) . j) + 0 by M15, X71, M23, DBLSEQ_3:def 15;
hence (Partial_Sums_in_cod1 (P * LG)) . ((len (P * D)),j) = (P * G) . j by XXREAL_3:4; :: thesis:

end;

then X120: M . (Union FSets) <= Sum (P * G) by X2, X100, DBLSEQ_3:41;
Partial_Sums (P * G) is non-decreasing by MESFUNC9:16;
then X123: Partial_Sums (P * G) is convergent by RINFSUP2:37;
X124: Partial_Sums (M * FSets) is subsequence of Partial_Sums (P * G)

proof

consider N being increasing sequence of NAT such that
Z0: for k being Nat holds N . k = ((Partial_Sums (Length s)) . k) - 1 by Th11;
defpred S₄[ Nat] means ((Partial_Sums (P * G)) * N) . $1 = (Partial_Sums (M * FSets)) . $1;
[0,(s . 0)] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } by F9;
then consider n0 being Nat, E0 being disjoint_valued FinSequence of S such that
Z1: ( [0,(s . 0)] = [n0,E0] & Union E0 = FSets . n0 & ( FSets . n0 = {} implies E0 = <*{}*> ) ) ;
Z2: ( n0 = 0 & E0 = s . 0 ) by Z1, XTUPLE_0:1;
Z4: M . (Union E0) = Sum (P * E0) by A1, Z1;
consider SPE0 being sequence of ExtREAL such that
Z5: ( Sum (P * E0) = SPE0 . (len (P * E0)) & SPE0 . 0 = 0. & ( for i being Nat st i < len (P * E0) holds
SPE0 . (i + 1) = (SPE0 . i) + ((P * E0) . (i + 1)) ) ) by EXTREAL1:def 2;
rng E0 c= S ;
then rng E0 c= dom P by FUNCT_2:def 1;
then ZZ10: dom (P * E0) = dom E0 by RELAT_1:27;
then Z10: len (P * E0) = len E0 by FINSEQ_3:29;
len (s . 0) >= 1 by FINSEQ_1:20;
then Z11: ( len (s . 0) in dom (s . 0) & 1 in dom (s . 0) ) by FINSEQ_3:25;
then consider N0 being Nat such that
Z6: ( N0 = ((((Partial_Sums (Length s)) . 0) - (len (s . 0))) + (len (s . 0))) - 1 & G . N0 = (s . 0) . (len (s . 0)) ) by Th13;
Z6d: N0 = N . 0 by Z0, Z6;
N0 = ((Length s) . 0) - 1 by Z6, SERIES_1:def 1;
then Z6c: N0 + 1 = len (s . 0) by Def3;
then Z6b: N0 < len (s . 0) by NAT_1:13;
defpred S₅[ Nat] means ( $1 < len (P * E0) implies (Partial_Sums (P * G)) . $1 = SPE0 . ($1 + 1) );
consider z0 being Nat such that
Z7: ( z0 = ((((Partial_Sums (Length s)) . 0) - (len (s . 0))) + 1) - 1 & G . z0 = (s . 0) . 1 ) by Z11, Th13;
z0 = ((Length s) . 0) - (len (s . 0)) by Z7, SERIES_1:def 1;
then Z8: z0 = (len (s . 0)) - (len (s . 0)) by Def3;
Z12: (Partial_Sums (P * G)) . 0 = (P * G) . 0 by MESFUNC9:def 1
.= P . ((s . 0) . 1) by Z7, Z8, FUNCT_2:15
.= (P * E0) . 1 by Z11, Z2, FUNCT_1:13 ;
SPE0 . (0 + 1) = 0 + ((P * E0) . 1) by Z5, Z10, Z2;
then ZZ1: S₅[ 0 ] by Z12, XXREAL_3:4;
ZZ2: for i being Nat st S₅[i] holds
S₅[i + 1]

proof

let i be Nat; :: thesis:
assume Z13: S₅[i] ; :: thesis:
assume Z14: i + 1 < len (P * E0) ; :: thesis:
Z16: (Partial_Sums (P * G)) . (i + 1) = ((Partial_Sums (P * G)) . i) + ((P * G) . (i + 1)) by MESFUNC9:def 1
.= (SPE0 . (i + 1)) + (P . (G . (i + 1))) by Z14, NAT_1:13, Z13, FUNCT_2:15 ;
Z18: ( 1 <= (i + 1) + 1 & (i + 1) + 1 <= len (P * E0) ) by Z14, NAT_1:11, NAT_1:13;
then consider zi1 being Nat such that
Z17: ( zi1 = ((((Partial_Sums (Length s)) . 0) - (len (s . 0))) + ((i + 1) + 1)) - 1 & G . zi1 = (s . 0) . ((i + 1) + 1) ) by Th13, ZZ10, Z2, FINSEQ_3:25;
zi1 = ((((Length s) . 0) - (len (s . 0))) + ((i + 1) + 1)) - 1 by Z17, SERIES_1:def 1
.= (((len (s . 0)) - (len (s . 0))) + ((i + 1) + 1)) - 1 by Def3 ;
then P . (G . (i + 1)) = (P * E0) . ((i + 1) + 1) by Z17, Z18, ZZ10, Z2, FINSEQ_3:25, FUNCT_1:13;
hence (Partial_Sums (P * G)) . (i + 1) = SPE0 . ((i + 1) + 1) by Z14, Z5, Z16; :: thesis:

end;

for i being Nat holds S₅[i] from NAT_1:sch 2(ZZ1, ZZ2);
then (Partial_Sums (P * G)) . N0 = M . (FSets . 0) by Z6b, Z6c, Z2, Z10, Z5, Z4, Z1;
then (Partial_Sums (P * G)) . N0 = (M * FSets) . 0 by FUNCT_2:15;
then (Partial_Sums (P * G)) . N0 = (Partial_Sums (M * FSets)) . 0 by MESFUNC9:def 1;
then Z100: S₄[ 0 ] by Z6d, FUNCT_2:15;
Z101: for n being Nat st S₄[n] holds
S₄[n + 1]

proof

let n be Nat; :: thesis:
assume Z20: S₄[n] ; :: thesis:
[(n + 1),(s . (n + 1))] in { [n,E] where n is Nat, E is disjoint_valued FinSequence of S : ( Union E = FSets . n & ( FSets . n = {} implies E = <*{}*> ) ) } by F9;
then consider N1 being Nat, E being disjoint_valued FinSequence of S such that
Z21: ( [(n + 1),(s . (n + 1))] = [N1,E] & Union E = FSets . N1 & ( FSets . N1 = {} implies E = <*{}*> ) ) ;
Z22: ( n + 1 = N1 & s . (n + 1) = E ) by Z21, XTUPLE_0:1;
Z24: M . (Union E) = Sum (P * E) by A1, Z21;
consider SPE being sequence of ExtREAL such that
Z25: ( Sum (P * E) = SPE . (len (P * E)) & SPE . 0 = 0. & ( for i being Nat st i < len (P * E) holds
SPE . (i + 1) = (SPE . i) + ((P * E) . (i + 1)) ) ) by EXTREAL1:def 2;
rng E c= S ;
then rng E c= dom P by FUNCT_2:def 1;
then ZZ30: dom (P * E) = dom E by RELAT_1:27;
then Z30: len (P * E) = len E by FINSEQ_3:29;
len (s . (n + 1)) >= 1 by FINSEQ_1:20;
then Z31: ( len (s . (n + 1)) in dom (s . (n + 1)) & 1 in dom (s . (n + 1)) ) by FINSEQ_3:25;
then consider NEnd being Nat such that
Z26: ( NEnd = ((((Partial_Sums (Length s)) . (n + 1)) - (len (s . (n + 1)))) + (len (s . (n + 1)))) - 1 & G . NEnd = (s . (n + 1)) . (len (s . (n + 1))) ) by Th13;
Z26d: NEnd = N . (n + 1) by Z0, Z26;
consider NSt being Nat such that
Z27: ( NSt = ((((Partial_Sums (Length s)) . (n + 1)) - (len (s . (n + 1)))) + 1) - 1 & G . NSt = (s . (n + 1)) . 1 ) by Z31, Th13;
NSt = (((Partial_Sums (Length s)) . n) + ((Length s) . (n + 1))) - (len (s . (n + 1))) by Z27, SERIES_1:def 1;
then Z28: NSt = (((Partial_Sums (Length s)) . n) + (len (s . (n + 1)))) - (len (s . (n + 1))) by Def3;
Z50: N . n = ((Partial_Sums (Length s)) . n) - 1 by Z0;
defpred S₆[ Nat] means ( $1 < len (P * E) implies (Partial_Sums (P * G)) . (((N . n) + $1) + 1) = ((Partial_Sums (P * G)) . (N . n)) + (SPE . ($1 + 1)) );
Z40: (Partial_Sums (P * G)) . ((N . n) + 1) = ((Partial_Sums (P * G)) . (N . n)) + ((P * G) . ((N . n) + 1)) by MESFUNC9:def 1
.= ((Partial_Sums (P * G)) . (N . n)) + (P . (G . ((N . n) + 1))) by FUNCT_2:15
.= ((Partial_Sums (P * G)) . (N . n)) + ((P * E) . 1) by Z31, Z22, Z50, Z28, Z27, FUNCT_1:13 ;
SPE . (0 + 1) = (SPE . 0) + ((P * E) . (0 + 1)) by Z25, Z30, Z22;
then Z60: S₆[ 0 ] by Z40, Z25, XXREAL_3:4;
Z61: for j being Nat st S₆[j] holds
S₆[j + 1]

proof

let j be Nat; :: thesis:
assume Z52: S₆[j] ; :: thesis:
assume Z53: j + 1 < len (P * E) ; :: thesis:
then Z58a: ( 1 <= (j + 1) + 1 & (j + 1) + 1 <= len (P * E) ) by NAT_1:11, NAT_1:13;
then consider Nj being Nat such that
Z58: ( Nj = ((((Partial_Sums (Length s)) . (n + 1)) - (len (s . (n + 1)))) + ((j + 1) + 1)) - 1 & G . Nj = (s . (n + 1)) . ((j + 1) + 1) ) by Th13, ZZ30, Z22, FINSEQ_3:25;
Z55: (Partial_Sums (P * G)) . (N . n) > -infty by SUPINF_2:51;
Z56: P . (G . ((((N . n) + j) + 1) + 1)) > -infty by SUPINF_2:51;
defpred S₇[ Nat] means ( $1 <= len (P * E) implies SPE . $1 >= 0 );
ZZ1: S₇[ 0 ] by Z25;
ZZ2: for t being Nat st S₇[t] holds
S₇[t + 1]

proof

let t be Nat; :: thesis:
assume ZZ3: S₇[t] ; :: thesis:
assume ZZ6: t + 1 <= len (P * E) ; :: thesis:
then ZZ5: SPE . (t + 1) = (SPE . t) + ((P * E) . (t + 1)) by Z25, NAT_1:13;
t + 1 in dom (P * E) by NAT_1:11, ZZ6, FINSEQ_3:25;
then (P * E) . (t + 1) = P . (E . (t + 1)) by FUNCT_1:12;
then (P * E) . (t + 1) >= 0 by SUPINF_2:51;
hence SPE . (t + 1) >= 0 by ZZ3, ZZ6, NAT_1:13, ZZ5; :: thesis:

end;

for t being Nat holds S₇[t] from NAT_1:sch 2(ZZ1, ZZ2);
then Z57: SPE . (j + 1) >= 0 by Z53;
(Partial_Sums (P * G)) . (((N . n) + (j + 1)) + 1) = ((Partial_Sums (P * G)) . ((N . n) + (j + 1))) + ((P * G) . (((N . n) + (j + 1)) + 1)) by MESFUNC9:def 1
.= (((Partial_Sums (P * G)) . (N . n)) + (SPE . (j + 1))) + (P . (G . ((((N . n) + j) + 1) + 1))) by Z53, Z52, NAT_1:13, FUNCT_2:15
.= ((Partial_Sums (P * G)) . (N . n)) + ((SPE . (j + 1)) + (P . (G . ((((N . n) + j) + 1) + 1)))) by Z55, Z56, Z57, XXREAL_3:29
.= ((Partial_Sums (P * G)) . (N . n)) + ((SPE . (j + 1)) + ((P * E) . ((j + 1) + 1))) by Z58a, Z58, Z50, Z28, Z27, Z22, ZZ30, FINSEQ_3:25, FUNCT_1:13 ;
hence (Partial_Sums (P * G)) . (((N . n) + (j + 1)) + 1) = ((Partial_Sums (P * G)) . (N . n)) + (SPE . ((j + 1) + 1)) by Z53, Z25; :: thesis:

end;

Z62: for j being Nat holds S₆[j] from NAT_1:sch 2(Z60, Z61);
Z59a: (N . n) + (len (P * E)) = (((Partial_Sums (Length s)) . n) - 1) + (len (s . (n + 1))) by Z0, Z30, Z22
.= (((Partial_Sums (Length s)) . n) - 1) + ((Length s) . (n + 1)) by Def3
.= (((Partial_Sums (Length s)) . n) + ((Length s) . (n + 1))) - 1
.= N . (n + 1) by Z26, Z26d, SERIES_1:def 1 ;
consider sn1 being Nat such that
Z63: len (P * E) = sn1 + 1 by Z22, Z30, NAT_1:6;
sn1 < len (P * E) by Z63, NAT_1:13;
then TA: (Partial_Sums (P * G)) . (((N . n) + sn1) + 1) = ((Partial_Sums (P * G)) . (N . n)) + (Sum (P * E)) by Z25, Z62, Z63
.= ((Partial_Sums (P * G)) . (N . n)) + ((M * FSets) . (n + 1)) by Z24, Z21, Z22, FUNCT_2:15 ;
(Partial_Sums (M * FSets)) . (n + 1) = (((Partial_Sums (P * G)) * N) . n) + ((M * FSets) . (n + 1)) by Z20, MESFUNC9:def 1
.= (Partial_Sums (P * G)) . (N . (n + 1)) by TA, Z59a, Z63, ORDINAL1:def 12, FUNCT_2:15
.= ((Partial_Sums (P * G)) * N) . (n + 1) by FUNCT_2:15 ;
hence S₄[n + 1] ; :: thesis:

end;

for n being Nat holds S₄[n] from NAT_1:sch 2(Z100, Z101);
then for n being Element of NAT holds (Partial_Sums (M * FSets)) . n = ((Partial_Sums (P * G)) * N) . n ;
hence Partial_Sums (M * FSets) is subsequence of Partial_Sums (P * G) by FUNCT_2:def 8; :: thesis:

end;

X125: Sum (M * FSets) = Sum (P * G)

proof

per cases by X123, MESFUNC5:def 11, MESFUNC9:8;

suppose L1: Partial_Sums (P * G) is convergent_to_+infty ; :: thesis:

then lim (Partial_Sums (M * FSets)) = +infty by X124, DBLSEQ_3:27;
then lim (Partial_Sums (M * FSets)) = lim (Partial_Sums (P * G)) by L1, MESFUNC9:7;
then Sum (M * FSets) = lim (Partial_Sums (P * G)) by MESFUNC9:def 3;
hence Sum (M * FSets) = Sum (P * G) by MESFUNC9:def 3; :: thesis:

end;

suppose Partial_Sums (P * G) is convergent_to_finite_number ; :: thesis:

then lim (Partial_Sums (M * FSets)) = lim (Partial_Sums (P * G)) by X124, DBLSEQ_3:26;
then Sum (M * FSets) = lim (Partial_Sums (P * G)) by MESFUNC9:def 3;
hence Sum (M * FSets) = Sum (P * G) by MESFUNC9:def 3; :: thesis:

end;

H0: Partial_Sums (M * FSets) is non-decreasing by MESFUNC9:16;
for n being Nat holds (Partial_Sums (M * FSets)) . n <= M . (union (rng FSets))

proof

let n be Nat; :: thesis:
H1: union (rng (FSets | (Segm (n + 1)))) in Field_generated_by S by Th58;
rng (FSets | (Segm (n + 1))) c= rng FSets by RELAT_1:70;
then M . (union (rng (FSets | (Segm (n + 1))))) <= M . (union (rng FSets)) by B0, H1, MEASURE1:8, ZFMISC_1:77;
hence (Partial_Sums (M * FSets)) . n <= M . (union (rng FSets)) by Th58; :: thesis:

end;

then lim (Partial_Sums (M * FSets)) <= M . (union (rng FSets)) by H0, RINFSUP2:37, MESFUNC9:9;
then Sum (M * FSets) <= M . (union (rng FSets)) by MESFUNC9:def 3;
then Sum (M * FSets) <= M . (Union FSets) by CARD_3:def 4;
then X126: M . (Union FSets) = Sum (M * FSets) by X125, X120, XXREAL_0:1;
Sum (M * FSets) = SUM (M * FSets) by MEASURE8:2;
hence SUM (M * FSets) = M . (union (rng FSets)) by X126, CARD_3:def 4; :: thesis:

end;

suppose LL1: rng FSets is empty-membered ; :: thesis:

then union (rng FSets) = {} by Th52;
then L2: M . (union (rng FSets)) = 0 by VALUED_0:def 19;
LL3: for n being Nat holds (M * FSets) . n = 0

proof

let n be Nat; :: thesis:
LL4: dom FSets = NAT by FUNCT_2:def 1;
then FSets . n in rng FSets by FUNCT_1:3, ORDINAL1:def 12;
then FSets . n = {} by LL1;
then (M * FSets) . n = M . {} by LL4, ORDINAL1:def 12, FUNCT_1:13;
hence (M * FSets) . n = 0 by VALUED_0:def 19; :: thesis:

end;

LL5: ( dom (Partial_Sums (M * FSets)) = NAT & dom (seq_const 0) = NAT ) by FUNCT_2:def 1;
for n being object st n in dom (Partial_Sums (M * FSets)) holds
(Partial_Sums (M * FSets)) . n = (seq_const 0) . n

proof

let n be object ; :: thesis:
assume n in dom (Partial_Sums (M * FSets)) ; :: thesis:
then reconsider n1 = n as Nat ;
defpred S₁[ Nat] means (Partial_Sums (M * FSets)) . $1 = 0 ;
(Partial_Sums (M * FSets)) . 0 = (M * FSets) . 0 by MESFUNC9:def 1;
then LL8: S₁[ 0 ] by LL3;
LL9: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume S₁[i] ; :: thesis:
then ((Partial_Sums (M * FSets)) . i) + ((M * FSets) . (i + 1)) = (M * FSets) . (i + 1) by XXREAL_3:4;
then (Partial_Sums (M * FSets)) . (i + 1) = (M * FSets) . (i + 1) by MESFUNC9:def 1;
hence S₁[i + 1] by LL3; :: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(LL8, LL9);
then (Partial_Sums (M * FSets)) . n1 = 0 ;
hence (Partial_Sums (M * FSets)) . n = (seq_const 0) . n ; :: thesis:

end;

then Partial_Sums (M * FSets) = seq_const 0 by LL5, FUNCT_1:def 11;
then L4: ( Partial_Sums (M * FSets) is convergent_to_finite_number & Partial_Sums (M * FSets) is convergent & lim (Partial_Sums (M * FSets)) = lim (seq_const 0) ) by RINFSUP2:14;
SUM (M * FSets) = Sum (M * FSets) by MEASURE8:2;
hence SUM (M * FSets) = M . (union (rng FSets)) by L2, L4, MESFUNC9:def 3; :: thesis:

end;

hence M is completely-additive by MEASURE8:def 11; :: thesis: