let A be non empty Subset of REAL; :: thesis: for F being Interval_Covering of A
for G being one-to-one FinSequence of bool REAL st rng G c= rng F holds
ex F1 being Interval_Covering of A st
( ( for n being Nat st n in dom G holds
G . n = F1 . n ) & vol F1 = vol F )
let F be Interval_Covering of A; :: thesis: for G being one-to-one FinSequence of bool REAL st rng G c= rng F holds
ex F1 being Interval_Covering of A st
( ( for n being Nat st n in dom G holds
G . n = F1 . n ) & vol F1 = vol F )
let G be one-to-one FinSequence of bool REAL; :: thesis: ( rng G c= rng F implies ex F1 being Interval_Covering of A st
( ( for n being Nat st n in dom G holds
G . n = F1 . n ) & vol F1 = vol F ) )
assume A1: rng G c= rng F ; :: thesis: ex F1 being Interval_Covering of A st
( ( for n being Nat st n in dom G holds
G . n = F1 . n ) & vol F1 = vol F )
defpred S1[ Nat] means ex F0 being Interval_Covering of A st
( ( for n being Nat st n in dom (G | $1) holds
(G | $1) . n = F0 . n ) & F0,F are_fiberwise_equipotent & vol F0 = vol F );
A2: S1[ 0 ]
proof
take F ; :: thesis: ( ( for n being Nat st n in dom (G | 0) holds
(G | 0) . n = F . n ) & F,F are_fiberwise_equipotent & vol F = vol F )
thus ( ( for n being Nat st n in dom (G | 0) holds
(G | 0) . n = F . n ) & F,F are_fiberwise_equipotent & vol F = vol F ) ; :: thesis: verum
end;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then consider F0 being Interval_Covering of A such that
A4: for n being Nat st n in dom (G | k) holds
(G | k) . n = F0 . n and
A5: F0,F are_fiberwise_equipotent and
A6: vol F0 = vol F ;
A7: dom F0 = NAT by FUNCT_2:def 1;
per cases ( len G <= k or len G > k ) ;
suppose A8: len G <= k ; :: thesis: S1[k + 1]
then len G < k + 1 by NAT_1:13;
then ( G | k = G & G | (k + 1) = G ) by A8, FINSEQ_1:58;
hence S1[k + 1] by A4, A5, A6; :: thesis: verum
end;
suppose A9: len G > k ; :: thesis: S1[k + 1]
then A10: len G >= k + 1 by NAT_1:13;
then A11: len (G | (k + 1)) = k + 1 by FINSEQ_1:59;
A12: k + 1 in dom G by A10, FINSEQ_3:25, NAT_1:11;
G . (k + 1) = (G | (Seg (k + 1))) . (k + 1) by FUNCT_1:49, FINSEQ_1:4;
then A13: G . (k + 1) = (G | (k + 1)) . (k + 1) by FINSEQ_1:def 16;
then A14: (G | (k + 1)) . (k + 1) in rng F by A1, A12, FUNCT_1:3;
rng F = rng F0 by A5, CLASSES1:75;
then consider M0 being Element of NAT such that
A15: (G | (k + 1)) . (k + 1) = F0 . M0 by A14, FUNCT_2:113;
A16: now :: thesis: ( 1 <= M0 implies not M0 <= k )
assume A17: ( 1 <= M0 & M0 <= k ) ; :: thesis: contradiction
then M0 <= len G by A9, XXREAL_0:2;
then A18: M0 in dom G by A17, FINSEQ_3:25;
then M0 in dom (G | (Seg k)) by A17, FINSEQ_1:1, RELAT_1:57;
then M0 in dom (G | k) by FINSEQ_1:def 16;
then (G | k) . M0 = F0 . M0 by A4;
then G . M0 = F0 . M0 by A17, FINSEQ_3:112;
then M0 = k + 1 by A12, A13, A15, A18, FUNCT_1:def 4;
hence contradiction by A17, NAT_1:13; :: thesis: verum
end;
per cases ( M0 = 0 or k + 1 <= M0 ) by A16, NAT_1:13, NAT_1:14;
suppose A19: M0 = 0 ; :: thesis: S1[k + 1]
consider F1 being sequence of (bool REAL) such that
A20: ( ( for n being Nat st n <> 0 & n <> k + 1 holds
F0 . n = F1 . n ) & F0 . 0 = F1 . (k + 1) & F0 . (k + 1) = F1 . 0 ) by Th46;
A21: dom F1 = NAT by FUNCT_2:def 1;
A22: for n being Nat st n in dom (G | (k + 1)) holds
(G | (k + 1)) . n = F1 . n
proof
let n be Nat; :: thesis: ( n in dom (G | (k + 1)) implies (G | (k + 1)) . n = F1 . n )
assume n in dom (G | (k + 1)) ; :: thesis: (G | (k + 1)) . n = F1 . n
then A23: ( 1 <= n & n <= k + 1 ) by A11, FINSEQ_3:25;
per cases ( n = k + 1 or n <> k + 1 ) ;
suppose n = k + 1 ; :: thesis: (G | (k + 1)) . n = F1 . n
hence (G | (k + 1)) . n = F1 . n by A15, A19, A20; :: thesis: verum
end;
suppose A24: n <> k + 1 ; :: thesis: (G | (k + 1)) . n = F1 . n
then A25: F0 . n = F1 . n by A20, A23;
n < k + 1 by A23, A24, XXREAL_0:1;
then A26: n <= k by NAT_1:13;
n <= len G by A10, A23, XXREAL_0:2;
then n in dom G by A23, FINSEQ_3:25;
then n in dom (G | (Seg k)) by A23, A26, FINSEQ_1:1, RELAT_1:57;
then A27: n in dom (G | k) by FINSEQ_1:def 16;
(G | (k + 1)) . n = G . n by A23, FINSEQ_3:112;
then (G | (k + 1)) . n = (G | k) . n by A26, FINSEQ_3:112;
hence (G | (k + 1)) . n = F1 . n by A4, A25, A27; :: thesis: verum
end;
end;
end;
for n being set st n <> 0 & n <> k + 1 & n in dom F0 holds
F0 . n = F1 . n by A20;
then A28: F0,F1 are_fiberwise_equipotent by A7, A20, A21, RFINSEQ:28;
then rng F1 = rng F by A5, CLASSES1:75, CLASSES1:76;
then A29: A c= union (rng F1) by MEASURE7:def 2;
for n being Element of NAT holds F1 . n is Interval
proof
let n be Element of NAT ; :: thesis: F1 . n is Interval
per cases ( ( n <> 0 & n <> k + 1 ) or n = 0 or n = k + 1 ) ;
suppose ( n <> 0 & n <> k + 1 ) ; :: thesis: F1 . n is Interval
then F1 . n = F0 . n by A20;
hence F1 . n is Interval ; :: thesis: verum
end;
suppose ( n = 0 or n = k + 1 ) ; :: thesis: F1 . n is Interval
hence F1 . n is Interval by A20; :: thesis: verum
end;
end;
end;
then reconsider F1 = F1 as Interval_Covering of A by A29, MEASURE7:def 2;
vol F1 = vol F by A6, A20, Th52;
hence S1[k + 1] by A5, A22, A28, CLASSES1:76; :: thesis: verum
end;
suppose A30: k + 1 <= M0 ; :: thesis: S1[k + 1]
consider F1 being sequence of (bool REAL) such that
A31: ( ( for n being Nat st n <> M0 & n <> k + 1 holds
F0 . n = F1 . n ) & F0 . M0 = F1 . (k + 1) & F0 . (k + 1) = F1 . M0 ) by Th46;
A32: dom F1 = NAT by FUNCT_2:def 1;
A33: for n being Nat st n in dom (G | (k + 1)) holds
(G | (k + 1)) . n = F1 . n
proof
let n be Nat; :: thesis: ( n in dom (G | (k + 1)) implies (G | (k + 1)) . n = F1 . n )
assume n in dom (G | (k + 1)) ; :: thesis: (G | (k + 1)) . n = F1 . n
then A34: ( 1 <= n & n <= k + 1 ) by A11, FINSEQ_3:25;
per cases ( n = k + 1 or n <> k + 1 ) ;
suppose n = k + 1 ; :: thesis: (G | (k + 1)) . n = F1 . n
hence (G | (k + 1)) . n = F1 . n by A15, A31; :: thesis: verum
end;
suppose A35: n <> k + 1 ; :: thesis: (G | (k + 1)) . n = F1 . n
then n < k + 1 by A34, XXREAL_0:1;
then A36: F0 . n = F1 . n by A30, A31;
n < k + 1 by A34, A35, XXREAL_0:1;
then A37: n <= k by NAT_1:13;
n <= len G by A10, A34, XXREAL_0:2;
then n in dom G by A34, FINSEQ_3:25;
then n in dom (G | (Seg k)) by A34, A37, FINSEQ_1:1, RELAT_1:57;
then A38: n in dom (G | k) by FINSEQ_1:def 16;
(G | (k + 1)) . n = G . n by A34, FINSEQ_3:112;
then (G | (k + 1)) . n = (G | k) . n by A37, FINSEQ_3:112;
hence (G | (k + 1)) . n = F1 . n by A4, A36, A38; :: thesis: verum
end;
end;
end;
for n being set st n <> M0 & n <> k + 1 & n in dom F0 holds
F0 . n = F1 . n by A31;
then A39: F0,F1 are_fiberwise_equipotent by A7, A31, A32, RFINSEQ:28;
then rng F1 = rng F by A5, CLASSES1:75, CLASSES1:76;
then A40: A c= union (rng F1) by MEASURE7:def 2;
for n being Element of NAT holds F1 . n is Interval
proof
let n be Element of NAT ; :: thesis: F1 . n is Interval
per cases ( ( n <> M0 & n <> k + 1 ) or n = M0 or n = k + 1 ) ;
suppose ( n <> M0 & n <> k + 1 ) ; :: thesis: F1 . n is Interval
then F1 . n = F0 . n by A31;
hence F1 . n is Interval ; :: thesis: verum
end;
suppose ( n = M0 or n = k + 1 ) ; :: thesis: F1 . n is Interval
hence F1 . n is Interval by A31; :: thesis: verum
end;
end;
end;
then reconsider F1 = F1 as Interval_Covering of A by A40, MEASURE7:def 2;
vol F1 = vol F by A6, A31, Th52;
hence S1[k + 1] by A5, A33, A39, CLASSES1:76; :: thesis: verum
end;
end;
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A2, A3);
 then A41: S1[ len G] ;
G | (len G) = G by FINSEQ_1:58;
hence ex F1 being Interval_Covering of A st
( ( for n being Nat st n in dom G holds
G . n = F1 . n ) & vol F1 = vol F ) by A41; :: thesis: verum