let F be disjoint_valued FinSequence of Family_of_Intervals ; :: thesis:
assume A1: Union F in Family_of_Intervals ; :: thesis:
defpred S₁[ Nat] means for H being disjoint_valued FinSequence of Family_of_Intervals st len H = $1 & Union H in Family_of_Intervals holds
ex G being disjoint_valued FinSequence of Family_of_Intervals st
( H,G are_fiberwise_equipotent & ( for n being Nat st n in dom G holds
( Union (G | n) in Family_of_Intervals & pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) ) ) );

now :: thesis:

let H be disjoint_valued FinSequence of Family_of_Intervals ; :: thesis:
assume that
A2: len H = 0 and
Union H in Family_of_Intervals ; :: thesis:
A3: H = {} by A2;
take G = H; :: thesis:
thus H,G are_fiberwise_equipotent ; :: thesis:
thus for n being Nat st n in dom G holds
( Union (G | n) in Family_of_Intervals & pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) ) by A3; :: thesis:

end;

then A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A6: S₁[k] ; :: thesis:

hereby :: thesis:

let H be disjoint_valued FinSequence of Family_of_Intervals ; :: thesis:
assume that
A7: len H = k + 1 and
A8: Union H in Family_of_Intervals ; :: thesis:
A9: H <> {} by A7;
ex I being Interval st Union H = I by A8, MEASUR10:def 1;
then consider N being Nat such that
A10: ( N in dom H & (Union H) \ (H . N) is Interval ) by A9, Th61;
1 <= len H by A7, NAT_1:11;
then A11: len H in dom H by FINSEQ_3:25;
reconsider H1 = (Swap (H,N,(len H))) | (Seg k) as FinSequence of Family_of_Intervals by FINSEQ_1:18;
A12: H, Swap (H,N,(len H)) are_fiberwise_equipotent by A10, A11, Th28;
then A13: len (Swap (H,N,(len H))) = k + 1 by A7, RFINSEQ:3;
then len ((Swap (H,N,(len H))) | k) = k by NAT_1:11, FINSEQ_1:59;
then A14: len H1 = k by FINSEQ_1:def 16;
for n, m being object st n <> m holds
H1 . n misses H1 . m

proof

let n, m be object ; :: thesis:
assume A15: n <> m ; :: thesis:

per cases ;

suppose A16: ( n in dom H1 & m in dom H1 ) ; :: thesis:

then reconsider n1 = n, m1 = m as Element of NAT ;
A17: ( 1 <= n1 & n1 <= k & 1 <= m1 & m1 <= k ) by A16, A14, FINSEQ_3:25;
then A18: ( n1 <> len H & m1 <> len H ) by A7, NAT_1:13;
k <= k + 1 by NAT_1:11;
then ( 1 <= n1 & n1 <= len H & 1 <= m1 & m1 <= len H ) by A7, A17, XXREAL_0:2;
then A19: ( n1 in dom H & m1 in dom H ) by FINSEQ_3:25;

per cases ;

suppose n1 = N ; :: thesis:

then ( (Swap (H,N,(len H))) . n1 = H . (len H) & (Swap (H,N,(len H))) . m1 = H . m1 ) by A15, A19, A18, A11, EXCHSORT:29, EXCHSORT:33;
then ( H1 . n1 = H . (len H) & H1 . m1 = H . m1 ) by A17, FINSEQ_1:1, FUNCT_1:49;
hence H1 . n misses H1 . m by A18, PROB_2:def 2; :: thesis:

end;

suppose m1 = N ; :: thesis:

then ( (Swap (H,N,(len H))) . m1 = H . (len H) & (Swap (H,N,(len H))) . n1 = H . n1 ) by A15, A19, A18, A11, EXCHSORT:29, EXCHSORT:33;
then ( H1 . m1 = H . (len H) & H1 . n1 = H . n1 ) by A17, FINSEQ_1:1, FUNCT_1:49;
hence H1 . n misses H1 . m by A18, PROB_2:def 2; :: thesis:

end;

suppose ( n1 <> N & m1 <> N ) ; :: thesis:

then ( (Swap (H,N,(len H))) . n1 = H . n1 & (Swap (H,N,(len H))) . m1 = H . m1 ) by A18, EXCHSORT:33;
then ( H1 . n1 = H . n1 & H1 . m1 = H . m1 ) by A17, FINSEQ_1:1, FUNCT_1:49;
hence H1 . n misses H1 . m by A15, PROB_2:def 2; :: thesis:

end;

suppose ( not n in dom H1 or not m in dom H1 ) ; :: thesis:

then ( H1 . n = {} or H1 . m = {} ) by FUNCT_1:def 2;
hence H1 . n misses H1 . m by XBOOLE_1:65; :: thesis:

end;

proof

let A be set ; :: thesis:
assume A in rng H1 ; :: thesis:
then consider n being Element of NAT such that
A24: ( n in dom H1 & A = H1 . n ) by PARTFUN1:3;
A25: ( 1 <= n & n <= k ) by A14, A24, FINSEQ_3:25;
then A26: A = (Swap (H,N,(len H))) . n by A24, FUNCT_1:49, FINSEQ_1:1;
A27: n <> len H by A7, A25, NAT_1:13;
n <= len H by A7, A25, NAT_1:13;
then A28: n in dom H by A25, FINSEQ_3:25;

per cases ;

suppose A29: n = N ; :: thesis:

then A = H . (len H) by A11, A26, A28, EXCHSORT:29;
hence A misses (Swap (H,N,(len H))) . (len H) by A22, A27, A29, PROB_2:def 2; :: thesis:

end;

suppose A30: n <> N ; :: thesis:

then A = H . n by A26, A27, EXCHSORT:33;
hence A misses (Swap (H,N,(len H))) . (len H) by A22, A30, PROB_2:def 2; :: thesis:

end;

then A31: union (rng H1) misses (Swap (H,N,(len H))) . (len H) by ZFMISC_1:80;
union (rng H1) = (union (rng H)) \ ((Swap (H,N,(len H))) . (len H)) by A23, A21, ZFMISC_1:80, XBOOLE_1:88;
then Union H1 = (union (rng H)) \ (H . N) by A22, CARD_3:def 4;
then Union H1 is Interval by A10, CARD_3:def 4;
then Union H1 in { I where I is Interval : verum } ;
then consider G1 being disjoint_valued FinSequence of Family_of_Intervals such that
A32: H1,G1 are_fiberwise_equipotent and
A33: for n being Nat st n in dom G1 holds
( Union (G1 | n) in Family_of_Intervals & pre-Meas . (Union (G1 | n)) = Sum (pre-Meas * (G1 | n)) ) by A6, A14, MEASUR10:def 1;
set G = G1 ^ <*(H . N)*>;
A34: H . N in rng H by A10, FUNCT_1:3;
then {(H . N)} c= Family_of_Intervals by ZFMISC_1:31;
then rng <*(H . N)*> c= Family_of_Intervals by FINSEQ_1:38;
then A35: <*(H . N)*> is disjoint_valued FinSequence of Family_of_Intervals by FINSEQ_1:def 4;
A36: union (rng G1) misses H . N by A31, A22, A32, CLASSES1:75;
for A being set st A in rng <*(H . N)*> holds
A misses union (rng G1)

proof

let A be set ; :: thesis:
assume A in rng <*(H . N)*> ; :: thesis:
then A in {(H . N)} by FINSEQ_1:38;
then A = H . N by TARSKI:def 1;
hence A misses union (rng G1) by A36; :: thesis:

end;

then union (rng G1) misses union (rng <*(H . N)*>) by ZFMISC_1:80;
then reconsider G = G1 ^ <*(H . N)*> as disjoint_valued FinSequence of Family_of_Intervals by A35, FINSEQ_1:75, MEASURE9:45;
take G = G; :: thesis:
A37: Swap (H,N,(len H)),G are_fiberwise_equipotent by A32, A20, A22, RFINSEQ:1;
hence A38: H,G are_fiberwise_equipotent by A12, CLASSES1:76; :: thesis:
thus for n being Nat st n in dom G holds
( Union (G | n) in Family_of_Intervals & pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) ) :: thesis:

proof

let n be Nat; :: thesis:
assume n in dom G ; :: thesis:
then A39: ( 1 <= n & n <= len G ) by FINSEQ_3:25;
A40: ( len G = len H & len G1 = len H1 ) by A38, A32, RFINSEQ:3;
then dom G1 = Seg k by A14, FINSEQ_1:def 3;
then G1 = G | (Seg k) by FINSEQ_1:21;
then A41: G1 = G | k by FINSEQ_1:def 16;

per cases ;

suppose A42: n <= k ; :: thesis:

end;

suppose n > k ; :: thesis:

then A45: n >= k + 1 by NAT_1:13;
then A46: G | n = G by A40, A7, FINSEQ_1:58;
then rng (G | n) = rng H by A37, A12, CLASSES1:76, CLASSES1:75;
then Union (G | n) = union (rng H) by CARD_3:def 4;
hence Union (G | n) in Family_of_Intervals by A8, CARD_3:def 4; :: thesis:
A47: Union G1 is Interval

proof

per cases ;

suppose k = 0 ; :: thesis:

then G1 = {} by A40;
then union (rng G1) = {} by ZFMISC_1:2;
then ( Union G1 = {} & {} c= REAL ) by CARD_3:def 4;
hence Union G1 is Interval ; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then k >= 1 by NAT_1:14;
then k in dom G1 by A14, A40, FINSEQ_3:25;
then Union (G1 | k) in { I where I is Interval : verum } by A33, MEASUR10:def 1;
then ex I being Interval st Union (G1 | k) = I ;
hence Union G1 is Interval by A14, A40, FINSEQ_1:58; :: thesis:

end;

then A48: Union G1 in { I where I is Interval : verum } ;
A49: rng <*(H . N)*> = {(H . N)} by FINSEQ_1:38;
then reconsider HN = <*(H . N)*> as FinSequence of Family_of_Intervals by A34, ZFMISC_1:31, FINSEQ_1:def 4;
A50: Union G1 misses H . N by A36, CARD_3:def 4;
rng (G | n) = (rng G1) \/ (rng <*(H . N)*>) by A46, FINSEQ_1:31;
then union (rng (G | n)) = (union (rng G1)) \/ (union (rng <*(H . N)*>)) by ZFMISC_1:78;
then A51: Union (G | n) = (union (rng G1)) \/ (union (rng <*(H . N)*>)) by CARD_3:def 4
.= (Union G1) \/ (union {(H . N)}) by A49, CARD_3:def 4 ;
rng G = rng H by A37, A12, CLASSES1:76, CLASSES1:75;
then Union G = union (rng H) by CARD_3:def 4;
then Union G = Union H by CARD_3:def 4;
then ex I being Interval st Union G = I by A8, MEASUR10:def 1;
then A52: (Union G1) \/ (H . N) is Interval by A51, A45, A40, A7, FINSEQ_1:58;
A53: pre-Meas . (Union G1) = Sum (pre-Meas * G1)

proof

per cases ;

suppose k = 0 ; :: thesis:

then A54: G1 = {} by A40;
then union (rng G1) = {} by ZFMISC_1:2;
then Union G1 = {} by CARD_3:def 4;
then pre-Meas . (Union G1) = diameter {} by A47, Th59;
then pre-Meas . (Union G1) = 0 by MEASURE5:def 6;
hence pre-Meas . (Union G1) = Sum (pre-Meas * G1) by A54, EXTREAL1:7; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then k >= 1 by NAT_1:14;
then A55: k in dom G1 by A14, A40, FINSEQ_3:25;
G1 | k = G1 by A14, A40, FINSEQ_1:58;
hence pre-Meas . (Union G1) = Sum (pre-Meas * G1) by A55, A33; :: thesis:

end;

A56: pre-Meas * HN = <*(pre-Meas . (H . N))*> by Th62;
reconsider LG1 = pre-Meas * G1 as FinSequence of ExtREAL ;
reconsider LHN = pre-Meas * HN as FinSequence of ExtREAL ;
dom pre-Meas = Family_of_Intervals by FUNCT_2:def 1;
then ( rng G1 c= dom pre-Meas & rng HN c= dom pre-Meas ) ;
then A57: pre-Meas * G = (pre-Meas * G1) ^ <*(pre-Meas . (H . N))*> by A56, MATRIX15:5;
pre-Meas . (Union (G | n)) = (pre-Meas . (Union G1)) + (pre-Meas . (H . N)) by A48, MEASUR10:def 1, A34, A50, A52, A51, Th60
.= Sum (pre-Meas * G) by A57, A53, MEASURE9:21 ;
hence pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) by A45, A40, A7, FINSEQ_1:58; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
then S₁[ len F] ;
hence ex G being disjoint_valued FinSequence of Family_of_Intervals st
( F,G are_fiberwise_equipotent & ( for n being Nat st n in dom G holds
( Union (G | n) in Family_of_Intervals & pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) ) ) ) by A1; :: thesis: