let X be non empty set ; :: thesis: for F being Field_Subset of X

for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds

for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F)

let F be Field_Subset of X; :: thesis: for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds

for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F)

let m be Measure of F; :: thesis: ( m is completely-additive & ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) implies for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F) )

A1: F c= sigma F by PROB_1:def 9;

assume m is completely-additive ; :: thesis: ( for Aseq being Set_Sequence of F holds

( ex n being Nat st not m . (Aseq . n) < +infty or not X = union (rng Aseq) ) or for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F) )

then consider M1 being sigma_Measure of (sigma F) such that

A2: M1 is_extension_of m and

A3: M1 = (sigma_Meas (C_Meas m)) | (sigma F) by Th33;

assume ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) ; :: thesis: for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F)

then consider Aseq being Set_Sequence of F such that

A4: for n being Nat holds m . (Aseq . n) < +infty and

A5: X = union (rng Aseq) ;

let M be sigma_Measure of (sigma F); :: thesis: ( M is_extension_of m implies M = (sigma_Meas (C_Meas m)) | (sigma F) )

reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Th15;

assume A6: M is_extension_of m ; :: thesis: M = (sigma_Meas (C_Meas m)) | (sigma F)

F c= sigma_Field (C_Meas m) by Th20;

then A7: sigma F c= sigma_Field (C_Meas m) by PROB_1:def 9;

A8: for B being Subset of X st B in sigma F holds

M . B <= M1 . B

M . B = M1 . B

M . B = M1 . B

for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds

for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F)

let F be Field_Subset of X; :: thesis: for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds

for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F)

let m be Measure of F; :: thesis: ( m is completely-additive & ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) implies for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F) )

A1: F c= sigma F by PROB_1:def 9;

assume m is completely-additive ; :: thesis: ( for Aseq being Set_Sequence of F holds

( ex n being Nat st not m . (Aseq . n) < +infty or not X = union (rng Aseq) ) or for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F) )

then consider M1 being sigma_Measure of (sigma F) such that

A2: M1 is_extension_of m and

A3: M1 = (sigma_Meas (C_Meas m)) | (sigma F) by Th33;

assume ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) ; :: thesis: for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F)

then consider Aseq being Set_Sequence of F such that

A4: for n being Nat holds m . (Aseq . n) < +infty and

A5: X = union (rng Aseq) ;

let M be sigma_Measure of (sigma F); :: thesis: ( M is_extension_of m implies M = (sigma_Meas (C_Meas m)) | (sigma F) )

reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Th15;

assume A6: M is_extension_of m ; :: thesis: M = (sigma_Meas (C_Meas m)) | (sigma F)

F c= sigma_Field (C_Meas m) by Th20;

then A7: sigma F c= sigma_Field (C_Meas m) by PROB_1:def 9;

A8: for B being Subset of X st B in sigma F holds

M . B <= M1 . B

proof

A18:
for B being set st ex k being Element of NAT st B c= Bseq . k & B in sigma F holds
let B be Subset of X; :: thesis: ( B in sigma F implies M . B <= M1 . B )

assume A9: B in sigma F ; :: thesis: M . B <= M1 . B

A10: for seq being Covering of B,F holds M . B <= SUM (vol (m,seq))

M . B <= r

then M . B <= inf (Svc (m,B)) by XXREAL_2:def 4;

then M . B <= (C_Meas m) . B by Def8;

then M . B <= (sigma_Meas (C_Meas m)) . B by A7, A9, MEASURE4:def 3;

hence M . B <= M1 . B by A3, A9, FUNCT_1:49; :: thesis: verum

end;assume A9: B in sigma F ; :: thesis: M . B <= M1 . B

A10: for seq being Covering of B,F holds M . B <= SUM (vol (m,seq))

proof

for r being ExtReal st r in Svc (m,B) holds
let seq be Covering of B,F; :: thesis: M . B <= SUM (vol (m,seq))

A11: for n being Element of NAT holds seq . n in sigma F by A1;

then reconsider seq1 = seq as SetSequence of sigma F by RELAT_1:def 19;

A14: rng seq1 c= sigma F ;

then reconsider Fseq = seq1 as sequence of (sigma F) by FUNCT_2:6;

B c= union (rng seq1) by Def3;

then ( Union seq1 in sigma F & B c= Union seq1 ) by CARD_3:def 4, PROB_1:17;

then A15: M . B <= M . (Union seq1) by A9, MEASURE1:31;

for n being object st n in NAT holds

(M * Fseq) . n = (vol (m,seq)) . n

rng Fseq is N_Sub_set_fam of X by MEASURE1:23;

then rng Fseq is N_Measure_fam of sigma F by A14, MEASURE2:def 1;

then M . (union (rng Fseq)) <= SUM (M * Fseq) by MEASURE2:11;

then M . (Union seq1) <= SUM (vol (m,seq)) by A17, CARD_3:def 4;

hence M . B <= SUM (vol (m,seq)) by A15, XXREAL_0:2; :: thesis: verum

end;A11: for n being Element of NAT holds seq . n in sigma F by A1;

now :: thesis: for y being object st y in rng seq holds

y in sigma F

then
rng seq c= sigma F
;y in sigma F

let y be object ; :: thesis: ( y in rng seq implies y in sigma F )

assume y in rng seq ; :: thesis: y in sigma F

then consider x being object such that

A12: x in NAT and

A13: seq . x = y by FUNCT_2:11;

thus y in sigma F by A11, A12, A13; :: thesis: verum

end;assume y in rng seq ; :: thesis: y in sigma F

then consider x being object such that

A12: x in NAT and

A13: seq . x = y by FUNCT_2:11;

thus y in sigma F by A11, A12, A13; :: thesis: verum

then reconsider seq1 = seq as SetSequence of sigma F by RELAT_1:def 19;

A14: rng seq1 c= sigma F ;

then reconsider Fseq = seq1 as sequence of (sigma F) by FUNCT_2:6;

B c= union (rng seq1) by Def3;

then ( Union seq1 in sigma F & B c= Union seq1 ) by CARD_3:def 4, PROB_1:17;

then A15: M . B <= M . (Union seq1) by A9, MEASURE1:31;

for n being object st n in NAT holds

(M * Fseq) . n = (vol (m,seq)) . n

proof

then A17:
SUM (M * Fseq) = SUM (vol (m,seq))
by FUNCT_2:12;
let n be object ; :: thesis: ( n in NAT implies (M * Fseq) . n = (vol (m,seq)) . n )

assume A16: n in NAT ; :: thesis: (M * Fseq) . n = (vol (m,seq)) . n

then reconsider n1 = n as Element of NAT ;

n1 in dom Fseq by A16, FUNCT_2:def 1;

then (M * Fseq) . n = M . (Fseq . n1) by FUNCT_1:13

.= m . (seq . n1) by A6 ;

hence (M * Fseq) . n = (vol (m,seq)) . n by Def5; :: thesis: verum

end;assume A16: n in NAT ; :: thesis: (M * Fseq) . n = (vol (m,seq)) . n

then reconsider n1 = n as Element of NAT ;

n1 in dom Fseq by A16, FUNCT_2:def 1;

then (M * Fseq) . n = M . (Fseq . n1) by FUNCT_1:13

.= m . (seq . n1) by A6 ;

hence (M * Fseq) . n = (vol (m,seq)) . n by Def5; :: thesis: verum

rng Fseq is N_Sub_set_fam of X by MEASURE1:23;

then rng Fseq is N_Measure_fam of sigma F by A14, MEASURE2:def 1;

then M . (union (rng Fseq)) <= SUM (M * Fseq) by MEASURE2:11;

then M . (Union seq1) <= SUM (vol (m,seq)) by A17, CARD_3:def 4;

hence M . B <= SUM (vol (m,seq)) by A15, XXREAL_0:2; :: thesis: verum

M . B <= r

proof

then
M . B is LowerBound of Svc (m,B)
by XXREAL_2:def 2;
let r be ExtReal; :: thesis: ( r in Svc (m,B) implies M . B <= r )

assume r in Svc (m,B) ; :: thesis: M . B <= r

then ex seq being Covering of B,F st r = SUM (vol (m,seq)) by Def7;

hence M . B <= r by A10; :: thesis: verum

end;assume r in Svc (m,B) ; :: thesis: M . B <= r

then ex seq being Covering of B,F st r = SUM (vol (m,seq)) by Def7;

hence M . B <= r by A10; :: thesis: verum

then M . B <= inf (Svc (m,B)) by XXREAL_2:def 4;

then M . B <= (C_Meas m) . B by Def8;

then M . B <= (sigma_Meas (C_Meas m)) . B by A7, A9, MEASURE4:def 3;

hence M . B <= M1 . B by A3, A9, FUNCT_1:49; :: thesis: verum

M . B = M1 . B

proof

for B being object st B in sigma F holds
let B be set ; :: thesis: ( ex k being Element of NAT st B c= Bseq . k & B in sigma F implies M . B = M1 . B )

assume ex k being Element of NAT st B c= Bseq . k ; :: thesis: ( not B in sigma F or M . B = M1 . B )

then consider k being Element of NAT such that

A19: B c= Bseq . k ;

A20: M . (Bseq . k) = m . (Bseq . k) by A6;

assume A21: B in sigma F ; :: thesis: M . B = M1 . B

then reconsider B9 = B as Subset of X ;

A22: ( F c= sigma F & Bseq . k in F ) by PROB_1:def 9;

then A23: (Bseq . k) \ B is Element of sigma F by A21, PROB_1:6;

then M . ((Bseq . k) \ B) <= M . (Bseq . k) by A22, MEASURE1:31, XBOOLE_1:36;

then A24: M . ((Bseq . k) \ B) < +infty by A4, A20, Th34, XXREAL_0:2;

(M . B) + (M . ((Bseq . k) \ B)) = M . (B \/ ((Bseq . k) \ B)) by A21, A23, MEASURE1:30, XBOOLE_1:79;

then (M . B) + (M . ((Bseq . k) \ B)) = M . ((Bseq . k) \/ B) by XBOOLE_1:39;

then A25: (M . B) + (M . ((Bseq . k) \ B)) = M . (Bseq . k) by A19, XBOOLE_1:12;

0 <= M . ((Bseq . k) \ B) by SUPINF_2:51;

then A26: M . B = (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A25, A24, XXREAL_3:28;

A27: M1 . (Bseq . k) = m . (Bseq . k) by A2;

(M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (B \/ ((Bseq . k) \ B)) by A21, A23, MEASURE1:30, XBOOLE_1:79;

then (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . ((Bseq . k) \/ B) by XBOOLE_1:39;

then A28: (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (Bseq . k) by A19, XBOOLE_1:12;

M1 . ((Bseq . k) \ B) <= M1 . (Bseq . k) by A22, A23, MEASURE1:31, XBOOLE_1:36;

then A29: M1 . ((Bseq . k) \ B) < +infty by A4, A27, Th34, XXREAL_0:2;

0 <= M1 . ((Bseq . k) \ B) by SUPINF_2:51;

then A30: M1 . B = (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) by A28, A29, XXREAL_3:28;

M . ((Bseq . k) \ B) <= M1 . ((Bseq . k) \ B) by A8, A21, A22, PROB_1:6;

then A31: (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) <= (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A27, A20, XXREAL_3:37;

M . B9 <= M1 . B9 by A8, A21;

hence M . B = M1 . B by A26, A30, A31, XXREAL_0:1; :: thesis: verum

end;assume ex k being Element of NAT st B c= Bseq . k ; :: thesis: ( not B in sigma F or M . B = M1 . B )

then consider k being Element of NAT such that

A19: B c= Bseq . k ;

A20: M . (Bseq . k) = m . (Bseq . k) by A6;

assume A21: B in sigma F ; :: thesis: M . B = M1 . B

then reconsider B9 = B as Subset of X ;

A22: ( F c= sigma F & Bseq . k in F ) by PROB_1:def 9;

then A23: (Bseq . k) \ B is Element of sigma F by A21, PROB_1:6;

then M . ((Bseq . k) \ B) <= M . (Bseq . k) by A22, MEASURE1:31, XBOOLE_1:36;

then A24: M . ((Bseq . k) \ B) < +infty by A4, A20, Th34, XXREAL_0:2;

(M . B) + (M . ((Bseq . k) \ B)) = M . (B \/ ((Bseq . k) \ B)) by A21, A23, MEASURE1:30, XBOOLE_1:79;

then (M . B) + (M . ((Bseq . k) \ B)) = M . ((Bseq . k) \/ B) by XBOOLE_1:39;

then A25: (M . B) + (M . ((Bseq . k) \ B)) = M . (Bseq . k) by A19, XBOOLE_1:12;

0 <= M . ((Bseq . k) \ B) by SUPINF_2:51;

then A26: M . B = (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A25, A24, XXREAL_3:28;

A27: M1 . (Bseq . k) = m . (Bseq . k) by A2;

(M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (B \/ ((Bseq . k) \ B)) by A21, A23, MEASURE1:30, XBOOLE_1:79;

then (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . ((Bseq . k) \/ B) by XBOOLE_1:39;

then A28: (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (Bseq . k) by A19, XBOOLE_1:12;

M1 . ((Bseq . k) \ B) <= M1 . (Bseq . k) by A22, A23, MEASURE1:31, XBOOLE_1:36;

then A29: M1 . ((Bseq . k) \ B) < +infty by A4, A27, Th34, XXREAL_0:2;

0 <= M1 . ((Bseq . k) \ B) by SUPINF_2:51;

then A30: M1 . B = (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) by A28, A29, XXREAL_3:28;

M . ((Bseq . k) \ B) <= M1 . ((Bseq . k) \ B) by A8, A21, A22, PROB_1:6;

then A31: (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) <= (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A27, A20, XXREAL_3:37;

M . B9 <= M1 . B9 by A8, A21;

hence M . B = M1 . B by A26, A30, A31, XXREAL_0:1; :: thesis: verum

M . B = M1 . B

proof

hence
M = (sigma_Meas (C_Meas m)) | (sigma F)
by A3, FUNCT_2:12; :: thesis: verum
let B be object ; :: thesis: ( B in sigma F implies M . B = M1 . B )

assume A32: B in sigma F ; :: thesis: M . B = M1 . B

then reconsider B9 = B as Subset of X ;

deffunc H_{1}( object ) -> Element of bool X = B9 /\ (Bseq . $1);

A33: for n being object st n in NAT holds

H_{1}(n) in bool X
;

consider Cseq being sequence of (bool X) such that

A34: for n being object st n in NAT holds

Cseq . n = H_{1}(n)
from FUNCT_2:sch 2(A33);

reconsider Cseq = Cseq as SetSequence of X ;

for n, m being Nat st n <= m holds

Cseq . n c= Cseq . m

then reconsider Cseq = Cseq as SetSequence of sigma F by RELAT_1:def 19;

for n being object st n in NAT holds

(M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n

for n being Nat holds Cseq . n = B9 /\ (Bseq . n) by ORDINAL1:def 12, A34;

then Cseq = B9 (/\) Bseq by SETLIM_2:def 5;

then Union Cseq = B9 /\ (Union Bseq) by SETLIM_2:38;

then Union Cseq = B9 /\ (Union Aseq) by PROB_3:15;

then Union Cseq = B9 /\ X by A5, CARD_3:def 4;

then A50: B9 = Union Cseq by XBOOLE_1:28;

then B9 = lim Cseq by A37, SETLIM_1:63;

then M1 . B = lim (M1 * Cseq) by A37, Th26;

then M1 . B = lim (M * (Partial_Union Cseq)) by A37, A49, PROB_4:19;

then M1 . B = lim (M * Cseq) by A37, PROB_4:19;

then M1 . B = M . (lim Cseq) by A37, Th26;

hence M1 . B = M . B by A37, A50, SETLIM_1:63; :: thesis: verum

end;assume A32: B in sigma F ; :: thesis: M . B = M1 . B

then reconsider B9 = B as Subset of X ;

deffunc H

A33: for n being object st n in NAT holds

H

consider Cseq being sequence of (bool X) such that

A34: for n being object st n in NAT holds

Cseq . n = H

reconsider Cseq = Cseq as SetSequence of X ;

for n, m being Nat st n <= m holds

Cseq . n c= Cseq . m

proof

then A37:
Cseq is non-descending
by PROB_1:def 5;
let n, m be Nat; :: thesis: ( n <= m implies Cseq . n c= Cseq . m )

A35: ( n in NAT & m in NAT ) by ORDINAL1:def 12;

A36: Bseq is non-descending by PROB_3:11;

assume n <= m ; :: thesis: Cseq . n c= Cseq . m

then Bseq . n c= Bseq . m by A36, PROB_1:def 5;

then B9 /\ (Bseq . n) c= B9 /\ (Bseq . m) by XBOOLE_1:26;

then Cseq . n c= B9 /\ (Bseq . m) by A34, A35;

hence Cseq . n c= Cseq . m by A34, A35; :: thesis: verum

end;A35: ( n in NAT & m in NAT ) by ORDINAL1:def 12;

A36: Bseq is non-descending by PROB_3:11;

assume n <= m ; :: thesis: Cseq . n c= Cseq . m

then Bseq . n c= Bseq . m by A36, PROB_1:def 5;

then B9 /\ (Bseq . n) c= B9 /\ (Bseq . m) by XBOOLE_1:26;

then Cseq . n c= B9 /\ (Bseq . m) by A34, A35;

hence Cseq . n c= Cseq . m by A34, A35; :: thesis: verum

now :: thesis: for y being object st y in rng Cseq holds

y in sigma F

then
rng Cseq c= sigma F
;y in sigma F

let y be object ; :: thesis: ( y in rng Cseq implies y in sigma F )

assume y in rng Cseq ; :: thesis: y in sigma F

then consider x being object such that

A38: x in NAT and

A39: Cseq . x = y by FUNCT_2:11;

reconsider x = x as Element of NAT by A38;

Bseq . x in F ;

then (Bseq . x) /\ B9 in sigma F by A1, A32, MEASURE1:34;

hence y in sigma F by A34, A39; :: thesis: verum

end;assume y in rng Cseq ; :: thesis: y in sigma F

then consider x being object such that

A38: x in NAT and

A39: Cseq . x = y by FUNCT_2:11;

reconsider x = x as Element of NAT by A38;

Bseq . x in F ;

then (Bseq . x) /\ B9 in sigma F by A1, A32, MEASURE1:34;

hence y in sigma F by A34, A39; :: thesis: verum

then reconsider Cseq = Cseq as SetSequence of sigma F by RELAT_1:def 19;

for n being object st n in NAT holds

(M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n

proof

then A49:
M1 * (Partial_Union Cseq) = M * (Partial_Union Cseq)
by FUNCT_2:12;
let n be object ; :: thesis: ( n in NAT implies (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n )

assume A40: n in NAT ; :: thesis: (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n

then reconsider n1 = n as Nat ;

A48: rng (Partial_Union Cseq) c= sigma F by RELAT_1:def 19;

dom (Partial_Union Cseq) = NAT by PARTFUN1:def 2;

then (Partial_Union Cseq) . n1 in rng (Partial_Union Cseq) by FUNCT_1:3, A40;

then (M1 * (Partial_Union Cseq)) . n = M . ((Partial_Union Cseq) . n1) by A47, A18, A44, A48, A40;

hence (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n by FUNCT_2:15, A40; :: thesis: verum

end;assume A40: n in NAT ; :: thesis: (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n

then reconsider n1 = n as Nat ;

A41: now :: thesis: for x being set st x in (Partial_Union Cseq) . n1 holds

ex k being Element of NAT st

( k <= n1 & x in Bseq . k )

A44:
(Partial_Union Cseq) . n1 c= Bseq . n1
ex k being Element of NAT st

( k <= n1 & x in Bseq . k )

let x be set ; :: thesis: ( x in (Partial_Union Cseq) . n1 implies ex k being Element of NAT st

( k <= n1 & x in Bseq . k ) )

assume x in (Partial_Union Cseq) . n1 ; :: thesis: ex k being Element of NAT st

( k <= n1 & x in Bseq . k )

then consider k being Nat such that

A42: k <= n1 and

A43: x in Cseq . k by PROB_3:13;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

take k = k; :: thesis: ( k <= n1 & x in Bseq . k )

x in B9 /\ (Bseq . k) by A34, A43;

hence ( k <= n1 & x in Bseq . k ) by A42, XBOOLE_0:def 4; :: thesis: verum

end;( k <= n1 & x in Bseq . k ) )

assume x in (Partial_Union Cseq) . n1 ; :: thesis: ex k being Element of NAT st

( k <= n1 & x in Bseq . k )

then consider k being Nat such that

A42: k <= n1 and

A43: x in Cseq . k by PROB_3:13;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

take k = k; :: thesis: ( k <= n1 & x in Bseq . k )

x in B9 /\ (Bseq . k) by A34, A43;

hence ( k <= n1 & x in Bseq . k ) by A42, XBOOLE_0:def 4; :: thesis: verum

proof

A47:
(M1 * (Partial_Union Cseq)) . n = M1 . ((Partial_Union Cseq) . n1)
by FUNCT_2:15, A40;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Partial_Union Cseq) . n1 or x in Bseq . n1 )

assume x in (Partial_Union Cseq) . n1 ; :: thesis: x in Bseq . n1

then consider k being Element of NAT such that

A45: k <= n1 and

A46: x in Bseq . k by A41;

Bseq is non-descending by PROB_3:11;

then Bseq . k c= Bseq . n1 by A45, PROB_1:def 5;

hence x in Bseq . n1 by A46; :: thesis: verum

end;assume x in (Partial_Union Cseq) . n1 ; :: thesis: x in Bseq . n1

then consider k being Element of NAT such that

A45: k <= n1 and

A46: x in Bseq . k by A41;

Bseq is non-descending by PROB_3:11;

then Bseq . k c= Bseq . n1 by A45, PROB_1:def 5;

hence x in Bseq . n1 by A46; :: thesis: verum

A48: rng (Partial_Union Cseq) c= sigma F by RELAT_1:def 19;

dom (Partial_Union Cseq) = NAT by PARTFUN1:def 2;

then (Partial_Union Cseq) . n1 in rng (Partial_Union Cseq) by FUNCT_1:3, A40;

then (M1 * (Partial_Union Cseq)) . n = M . ((Partial_Union Cseq) . n1) by A47, A18, A44, A48, A40;

hence (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n by FUNCT_2:15, A40; :: thesis: verum

for n being Nat holds Cseq . n = B9 /\ (Bseq . n) by ORDINAL1:def 12, A34;

then Cseq = B9 (/\) Bseq by SETLIM_2:def 5;

then Union Cseq = B9 /\ (Union Bseq) by SETLIM_2:38;

then Union Cseq = B9 /\ (Union Aseq) by PROB_3:15;

then Union Cseq = B9 /\ X by A5, CARD_3:def 4;

then A50: B9 = Union Cseq by XBOOLE_1:28;

then B9 = lim Cseq by A37, SETLIM_1:63;

then M1 . B = lim (M1 * Cseq) by A37, Th26;

then M1 . B = lim (M * (Partial_Union Cseq)) by A37, A49, PROB_4:19;

then M1 . B = lim (M * Cseq) by A37, PROB_4:19;

then M1 . B = M . (lim Cseq) by A37, Th26;

hence M1 . B = M . B by A37, A50, SETLIM_1:63; :: thesis: verum