let A be non empty closed_interval Subset of REAL; :: thesis: for F being FinSequence of bool REAL st A c= union (rng F) & ( for n being Nat st n in dom F holds
A meets F . n ) & ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) holds
ex G being FinSequence of bool REAL st
( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len G holds
union (rng (G | n)) meets G . (n + 1) ) )
let F be FinSequence of bool REAL; :: thesis: ( A c= union (rng F) & ( for n being Nat st n in dom F holds
A meets F . n ) & ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) implies ex G being FinSequence of bool REAL st
( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len G holds
union (rng (G | n)) meets G . (n + 1) ) ) )
assume that
A1: A c= union (rng F) and
A2: for n being Nat st n in dom F holds
A meets F . n and
A3: for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ; :: thesis: ex G being FinSequence of bool REAL st
( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len G holds
union (rng (G | n)) meets G . (n + 1) ) )
defpred S₁[ Nat] means ( $1 <= len F implies ex G being FinSequence of bool REAL st
( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < $1 holds
union (rng (G | n)) meets G . (n + 1) ) ) );
union (rng F) <> {} by A1;
then A4: F <> {} by ZFMISC_1:2;
for n being Nat st 1 <= n & n < 1 holds
union (rng (F | n)) meets F . (n + 1) ;
then A5: S₁[1] ;
A6: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
assume A8: k + 1 <= len F ; :: thesis: ex G being FinSequence of bool REAL st
( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < k + 1 holds
union (rng (G | n)) meets G . (n + 1) ) )
then A9: k < len F by NAT_1:13;
consider G being FinSequence of bool REAL such that
A10: F,G are_fiberwise_equipotent and
A11: for n being Nat st 1 <= n & n < k holds
union (rng (G | n)) meets G . (n + 1) by A7, A8, NAT_1:13;
set G1 = G | k;
A12: rng F = rng G by A10, CLASSES1:75;
A13: len F = len G by A10, RFINSEQ:3;
then A14: len (G | k) = k by A9, FINSEQ_1:59;
rng (G | k) = rng (G | (Seg k)) by FINSEQ_1:def 16;
then A15: rng (G | k) c= rng G by RELAT_1:70;
A16: for n being Nat st n in dom (G | k) holds
(G | k) . n is open_interval Subset of REAL

proof

let n be Nat; :: thesis: ( n in dom (G | k) implies (G | k) . n is open_interval Subset of REAL )
assume n in dom (G | k) ; :: thesis: (G | k) . n is open_interval Subset of REAL
then (G | k) . n in rng G by A15, FUNCT_1:3;
then ex m being Element of NAT st
( m in dom F & (G | k) . n = F . m ) by A12, PARTFUN1:3;
hence (G | k) . n is open_interval Subset of REAL by A3; :: thesis: verum

end;

A17: for n being Nat st 1 <= n & n < len (G | k) holds
union (rng ((G | k) | n)) meets (G | k) . (n + 1)

proof

let n be Nat; :: thesis: ( 1 <= n & n < len (G | k) implies union (rng ((G | k) | n)) meets (G | k) . (n + 1) )
assume A18: ( 1 <= n & n < len (G | k) ) ; :: thesis: union (rng ((G | k) | n)) meets (G | k) . (n + 1)
then n + 1 <= len (G | k) by NAT_1:13;
then ( (G | k) . (n + 1) = G . (n + 1) & (G | k) | n = G | n ) by A14, A18, FINSEQ_3:112, FINSEQ_1:82;
hence union (rng ((G | k) | n)) meets (G | k) . (n + 1) by A11, A14, A18; :: thesis: verum

end;

now :: thesis: ex m being Nat st
( m > k & not union (rng (G | k)) misses G . m )

assume A19: for m being Nat st m > k holds
union (rng (G | k)) misses G . m ; :: thesis: contradiction
union (rng ((G | k) | (len (G | k)))) is open_interval Subset of REAL by A16, A17, Th40;
then union (rng (G | k)) is open_interval Subset of REAL by FINSEQ_1:58;
then consider x, y being R_eal such that
A20: union (rng (G | k)) = ].x,y.[ by MEASURE5:def 2;
consider a1, a2 being Real such that
A21: ( a1 <= a2 & A = [.a1,a2.] ) by MEASURE5:14;
A22: (G | k) . 1 = G . 1 by NAT_1:14, FINSEQ_3:112;
1 <= len F by A4, FINSEQ_1:20;
then 1 in dom G by A13, FINSEQ_3:25;
then ex m being Element of NAT st
( m in dom F & (G | k) . 1 = F . m ) by A12, A22, FUNCT_1:3, PARTFUN1:3;
then A23: A meets (G | k) . 1 by A2;
1 <= k by NAT_1:14;
then 1 in dom (G | k) by A14, FINSEQ_3:25;
then (G | k) . 1 in rng (G | k) by FUNCT_1:3;
then A24: A meets union (rng (G | k)) by A23, XBOOLE_1:63, ZFMISC_1:74;
then A25: ( x < a2 & a1 < y ) by A20, A21, XXREAL_1:89, XXREAL_1:93;
A26: union (rng (G | k)) <> {} by A24, XBOOLE_1:65;
then A27: x < y by A20, XXREAL_1:28;

per cases ( a1 <= x or ( x < a1 & y <= a2 ) or ( x < a1 & a2 < y ) ) ;

suppose a1 <= x ; :: thesis: contradiction

then x in A by A21, A25, XXREAL_1:1;
then consider P being set such that
A28: ( x in P & P in rng F ) by A1, TARSKI:def 4;
consider m being Element of NAT such that
A29: ( m in dom G & P = G . m ) by A12, A28, PARTFUN1:3;
ex i being Element of NAT st
( i in dom F & P = F . i ) by A28, PARTFUN1:3;
then G . m is open_interval Subset of REAL by A3, A29;
then consider p, q being R_eal such that
A30: G . m = ].p,q.[ by MEASURE5:def 2;
A31: ( p < x & x < q ) by A28, A29, A30, XXREAL_1:4;
A32: not x in union (rng (G | k)) by A20, XXREAL_1:4;

A33: now :: thesis: not m <= k

assume A34: m <= k ; :: thesis: contradiction
then A35: G . m = (G | k) . m by FINSEQ_3:112;
1 <= m by A29, FINSEQ_3:25;
then m in dom (G | k) by A14, A34, FINSEQ_3:25;
then P in rng (G | k) by A29, A35, FUNCT_1:3;
hence contradiction by A28, A32, TARSKI:def 4; :: thesis: verum

end;

per cases ( q <= y or q > y ) ;

suppose q <= y ; :: thesis: contradiction

then ( max (x,p) = x & min (y,q) = q ) by A31, XXREAL_0:def 9, XXREAL_0:def 10;
then (union (rng (G | k))) /\ (G . m) = ].x,q.[ by A20, A30, XXREAL_1:142;
then (union (rng (G | k))) /\ (G . m) <> {} by A31, XXREAL_1:33;
hence contradiction by A19, A33, XBOOLE_0:def 7; :: thesis: verum

end;

suppose q > y ; :: thesis: contradiction

then ( max (x,p) = x & min (y,q) = y ) by A31, XXREAL_0:def 9, XXREAL_0:def 10;
then (union (rng (G | k))) /\ (G . m) = ].x,y.[ by A20, A30, XXREAL_1:142;
hence contradiction by A19, A20, A26, A33, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

suppose ( x < a1 & y <= a2 ) ; :: thesis: contradiction

then y in A by A21, A25, XXREAL_1:1;
then consider P being set such that
A36: ( y in P & P in rng F ) by A1, TARSKI:def 4;
consider m being Element of NAT such that
A37: ( m in dom G & P = G . m ) by A12, A36, PARTFUN1:3;
ex i being Element of NAT st
( i in dom F & P = F . i ) by A36, PARTFUN1:3;
then G . m is open_interval Subset of REAL by A3, A37;
then consider p, q being R_eal such that
A38: G . m = ].p,q.[ by MEASURE5:def 2;
A39: not y in union (rng (G | k)) by A20, XXREAL_1:4;

A40: now :: thesis: not m <= k

assume A41: m <= k ; :: thesis: contradiction
then A42: G . m = (G | k) . m by FINSEQ_3:112;
1 <= m by A37, FINSEQ_3:25;
then m in dom (G | k) by A14, A41, FINSEQ_3:25;
then P in rng (G | k) by A37, A42, FUNCT_1:3;
hence contradiction by A36, A39, TARSKI:def 4; :: thesis: verum

end;

A43: ( p < y & y < q ) by A36, A37, A38, XXREAL_1:4;
then min (y,q) = y by XXREAL_0:def 9;
then (union (rng (G | k))) /\ (G . m) = ].(max (x,p)),y.[ by A20, A38, XXREAL_1:142;
then (union (rng (G | k))) /\ (G . m) <> {} by A27, A43, XXREAL_0:29, XXREAL_1:33;
hence contradiction by A19, A40, XBOOLE_0:def 7; :: thesis: verum

end;

suppose ( x < a1 & a2 < y ) ; :: thesis: contradiction

then A44: A c= union (rng (G | k)) by A20, A21, XXREAL_1:47;
k + 1 in dom G by A8, A13, FINSEQ_3:25, NAT_1:11;
then ex m being Element of NAT st
( m in dom F & G . (k + 1) = F . m ) by A12, FUNCT_1:3, PARTFUN1:3;
then A meets G . (k + 1) by A2;
then A45: (union (rng (G | k))) /\ (G . (k + 1)) <> {} by A44, XBOOLE_1:65, XBOOLE_1:77;
k + 1 > k by NAT_1:13;
hence contradiction by A19, A45, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

then consider M being Nat such that
A46: ( M > k & union (rng (G | k)) meets G . M ) ;

A47: now :: thesis: M in dom G

assume not M in dom G ; :: thesis: contradiction
then G . M = {} by FUNCT_1:def 2;
hence contradiction by A46, XBOOLE_1:65; :: thesis: verum

end;

reconsider H = Swap (G,(k + 1),M) as FinSequence of bool REAL ;
k + 1 in dom G by A8, A13, NAT_1:11, FINSEQ_3:25;
then A48: G, Swap (G,(k + 1),M) are_fiberwise_equipotent by A47, Th28;
for n being Nat st 1 <= n & n < k + 1 holds
union (rng (H | n)) meets H . (n + 1)

proof

let n be Nat; :: thesis: ( 1 <= n & n < k + 1 implies union (rng (H | n)) meets H . (n + 1) )
assume A49: ( 1 <= n & n < k + 1 ) ; :: thesis: union (rng (H | n)) meets H . (n + 1)

per cases ( n < k or n >= k ) ;

suppose A50: n < k ; :: thesis: union (rng (H | n)) meets H . (n + 1)

then A51: n + 1 <= k by NAT_1:13;
( n + 1 <> k + 1 & n + 1 <> M ) by A46, A50, NAT_1:13;
then H . (n + 1) = G . (n + 1) by EXCHSORT:33;
then A52: H . (n + 1) = (G | k) . (n + 1) by A51, FINSEQ_3:112;
n < M by A46, A50, XXREAL_0:2;
then ( not k + 1 in Seg n & not M in Seg n ) by A49, FINSEQ_1:1;
then H | (Seg n) = G | (Seg n) by Th29;
then H | n = G | (Seg n) by FINSEQ_1:def 16;
then A53: H | n = G | n by FINSEQ_1:def 16;
( (G | k) | n = (G | k) | n & (G | k) | n = G | n ) by A50, FINSEQ_1:82;
hence union (rng (H | n)) meets H . (n + 1) by A14, A17, A49, A50, A52, A53; :: thesis: verum

end;

suppose A54: n >= k ; :: thesis: union (rng (H | n)) meets H . (n + 1)

n <= k by A49, NAT_1:13;
then A55: n = k by A54, XXREAL_0:1;
then ( not k + 1 in Seg n & not M in Seg n ) by A46, A49, FINSEQ_1:1;
then H | (Seg n) = G | (Seg n) by Th29;
then H | n = G | (Seg n) by FINSEQ_1:def 16;
then A56: union (rng (H | n)) meets G . M by A46, A55, FINSEQ_1:def 16;
( 1 <= k + 1 & k + 1 <= len G ) by A8, A10, A49, RFINSEQ:3, XXREAL_0:2;
then k + 1 in dom G by FINSEQ_3:25;
hence union (rng (H | n)) meets H . (n + 1) by A47, A55, A56, EXCHSORT:29; :: thesis: verum

end;

end;

end;

hence ex G being FinSequence of bool REAL st
( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < k + 1 holds
union (rng (G | n)) meets G . (n + 1) ) ) by A10, A48, CLASSES1:76; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A5, A6);
then consider G being FinSequence of bool REAL such that
A57: ( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len F holds
union (rng (G | n)) meets G . (n + 1) ) ) by A4;
len F = len G by A57, RFINSEQ:3;
hence ex G being FinSequence of bool REAL st
( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len G holds
union (rng (G | n)) meets G . (n + 1) ) ) by A57; :: thesis: verum