defpred S1[ Element of REAL d, Element of REAL d] means ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & \$1 . i < \$2 . i & [(\$1 . i),(\$2 . i)] is Gap of G . i ) or ( not i in X & \$1 . i = \$2 . i & \$1 . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( \$2 . i < \$1 . i & [(\$1 . i),(\$2 . i)] is Gap of G . i ) ) ) );
deffunc H2( Element of REAL d, Element of REAL d) -> non empty Subset of (REAL d) = cell (\$1,\$2);
set CELLS = { H2(l,r) where l, r is Element of REAL d : S1[l,r] } ;
reconsider X = Seg k as Subset of (Seg d) by ;
defpred S2[ Element of Seg d, Element of ] means ( ( \$1 in X & ex li, ri being Real st
( \$2 = [li,ri] & li < ri & \$2 is Gap of G . \$1 ) ) or ( not \$1 in X & ex li being Real st
( \$2 = [li,li] & li in G . \$1 ) ) );
A2: now :: thesis: for i being Element of Seg d ex lri being Element of st S2[i,lri]
let i be Element of Seg d; :: thesis: ex lri being Element of st S2[i,lri]
thus ex lri being Element of st S2[i,lri] :: thesis: verum
proof
per cases ( i in X or not i in X ) ;
suppose A3: i in X ; :: thesis: ex lri being Element of st S2[i,lri]
consider li, ri being Real such that
A4: li in G . i and
A5: ri in G . i and
A6: li < ri and
A7: for xi being Real st xi in G . i & li < xi holds
not xi < ri by Th11;
reconsider li = li, ri = ri as Element of REAL by XREAL_0:def 1;
take [li,ri] ; :: thesis: S2[i,[li,ri]]
[li,ri] is Gap of G . i by A4, A5, A6, A7, Def5;
hence S2[i,[li,ri]] by A3, A6; :: thesis: verum
end;
suppose A8: not i in X ; :: thesis: ex lri being Element of st S2[i,lri]
set li = the Element of G . i;
reconsider li = the Element of G . i as Element of REAL ;
reconsider lri = [li,li] as Element of ;
take lri ; :: thesis: S2[i,lri]
thus S2[i,lri] by A8; :: thesis: verum
end;
end;
end;
end;
consider lr being Function of (Seg d), such that
A9: for i being Element of Seg d holds S2[i,lr . i] from deffunc H3( Element of Seg d) -> Element of REAL = (lr . \$1) `1 ;
consider l being Function of (Seg d),REAL such that
A10: for i being Element of Seg d holds l . i = H3(i) from deffunc H4( Element of Seg d) -> Element of REAL = (lr . \$1) `2 ;
consider r being Function of (Seg d),REAL such that
A11: for i being Element of Seg d holds r . i = H4(i) from reconsider l = l, r = r as Element of REAL d by Def3;
A12: now :: thesis: for i being Element of Seg d holds lr . i = [(l . i),(r . i)]
let i be Element of Seg d; :: thesis: lr . i = [(l . i),(r . i)]
A13: l . i = (lr . i) `1 by A10;
r . i = (lr . i) `2 by A11;
hence lr . i = [(l . i),(r . i)] by ; :: thesis: verum
end;
now :: thesis: ex A being non empty Subset of (REAL d) st
( A = cell (l,r) & ex l, r being Element of REAL d st
( A = cell (l,r) & ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )
take A = cell (l,r); :: thesis: ( A = cell (l,r) & ex l, r being Element of REAL d st
( A = cell (l,r) & ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )

thus A = cell (l,r) ; :: thesis: ex l, r being Element of REAL d st
( A = cell (l,r) & ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

now :: thesis: ex X being Subset of (Seg d) st
( card X = k & ex l, r being Element of REAL d st
( A = cell (l,r) & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) )
take X = X; :: thesis: ( card X = k & ex l, r being Element of REAL d st
( A = cell (l,r) & ( for i being Element of Seg d holds
( ( b7 in b4 & b5 . b7 < b6 . b7 & [(b5 . b7),(b6 . b7)] is Gap of G . b7 ) or ( not b7 in b4 & b5 . b7 = b6 . b7 & b5 . b7 in G . b7 ) ) ) ) )

thus card X = k by FINSEQ_1:57; :: thesis: ex l, r being Element of REAL d st
( A = cell (l,r) & ( for i being Element of Seg d holds
( ( b7 in b4 & b5 . b7 < b6 . b7 & [(b5 . b7),(b6 . b7)] is Gap of G . b7 ) or ( not b7 in b4 & b5 . b7 = b6 . b7 & b5 . b7 in G . b7 ) ) ) )

take l = l; :: thesis: ex r being Element of REAL d st
( A = cell (l,r) & ( for i being Element of Seg d holds
( ( b6 in b3 & b4 . b6 < b5 . b6 & [(b4 . b6),(b5 . b6)] is Gap of G . b6 ) or ( not b6 in b3 & b4 . b6 = b5 . b6 & b4 . b6 in G . b6 ) ) ) )

take r = r; :: thesis: ( A = cell (l,r) & ( for i being Element of Seg d holds
( ( b5 in b2 & b3 . b5 < b4 . b5 & [(b3 . b5),(b4 . b5)] is Gap of G . b5 ) or ( not b5 in b2 & b3 . b5 = b4 . b5 & b3 . b5 in G . b5 ) ) ) )

thus A = cell (l,r) ; :: thesis: for i being Element of Seg d holds
( ( b5 in b2 & b3 . b5 < b4 . b5 & [(b3 . b5),(b4 . b5)] is Gap of G . b5 ) or ( not b5 in b2 & b3 . b5 = b4 . b5 & b3 . b5 in G . b5 ) )

let i be Element of Seg d; :: thesis: ( ( b4 in b1 & b2 . b4 < b3 . b4 & [(b2 . b4),(b3 . b4)] is Gap of G . b4 ) or ( not b4 in b1 & b2 . b4 = b3 . b4 & b2 . b4 in G . b4 ) )
per cases ( i in X or not i in X ) ;
suppose A14: i in X ; :: thesis: ( ( b4 in b1 & b2 . b4 < b3 . b4 & [(b2 . b4),(b3 . b4)] is Gap of G . b4 ) or ( not b4 in b1 & b2 . b4 = b3 . b4 & b2 . b4 in G . b4 ) )
then consider li, ri being Real such that
A15: lr . i = [li,ri] and
A16: li < ri and
A17: lr . i is Gap of G . i by A9;
A18: lr . i = [(l . i),(r . i)] by A12;
then li = l . i by ;
hence ( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) by ; :: thesis: verum
end;
suppose A19: not i in X ; :: thesis: ( ( b4 in b1 & b2 . b4 < b3 . b4 & [(b2 . b4),(b3 . b4)] is Gap of G . b4 ) or ( not b4 in b1 & b2 . b4 = b3 . b4 & b2 . b4 in G . b4 ) )
then consider li being Real such that
A20: lr . i = [li,li] and
A21: li in G . i by A9;
A22: [li,li] = [(l . i),(r . i)] by ;
then li = l . i by XTUPLE_0:1;
hence ( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) by ; :: thesis: verum
end;
end;
end;
hence ex l, r being Element of REAL d st
( A = cell (l,r) & ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) ; :: thesis: verum
end;
then A23: cell (l,r) in { H2(l,r) where l, r is Element of REAL d : S1[l,r] } ;
defpred S3[ object , Element of REAL d, Element of REAL d, object ] means ( \$2 in product G & \$3 in product G & ( ( \$4 = [0,[\$2,\$3]] & \$1 = cell (\$2,\$3) ) or ( \$4 = [1,[\$2,\$3]] & \$1 = cell (\$2,\$3) ) ) );
defpred S4[ object , object ] means ex l, r being Element of REAL d st S3[\$1,l,r,\$2];
A24: for A being object st A in { H2(l,r) where l, r is Element of REAL d : S1[l,r] } holds
ex lr being object st S4[A,lr]
proof
let A be object ; :: thesis: ( A in { H2(l,r) where l, r is Element of REAL d : S1[l,r] } implies ex lr being object st S4[A,lr] )
assume A in { H2(l,r) where l, r is Element of REAL d : S1[l,r] } ; :: thesis: ex lr being object st S4[A,lr]
then consider l, r being Element of REAL d such that
A25: A = cell (l,r) and
A26: ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ;
per cases ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
by A26;
suppose A27: ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) ; :: thesis: ex lr being object st S4[A,lr]
take [0,[l,r]] ; :: thesis: S4[A,[0,[l,r]]]
take l ; :: thesis: ex r being Element of REAL d st S3[A,l,r,[0,[l,r]]]
take r ; :: thesis: S3[A,l,r,[0,[l,r]]]
now :: thesis: for i being Element of Seg d holds
( l . i in G . i & r . i in G . i )
let i be Element of Seg d; :: thesis: ( l . i in G . i & r . i in G . i )
( ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( l . i = r . i & l . i in G . i ) ) by A27;
hence ( l . i in G . i & r . i in G . i ) by Th13; :: thesis: verum
end;
hence ( l in product G & r in product G ) by Th8; :: thesis: ( ( [0,[l,r]] = [0,[l,r]] & A = cell (l,r) ) or ( [0,[l,r]] = [1,[l,r]] & A = cell (l,r) ) )
thus ( ( [0,[l,r]] = [0,[l,r]] & A = cell (l,r) ) or ( [0,[l,r]] = [1,[l,r]] & A = cell (l,r) ) ) by A25; :: thesis: verum
end;
suppose A28: ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: ex lr being object st S4[A,lr]
take [1,[l,r]] ; :: thesis: S4[A,[1,[l,r]]]
take l ; :: thesis: ex r being Element of REAL d st S3[A,l,r,[1,[l,r]]]
take r ; :: thesis: S3[A,l,r,[1,[l,r]]]
now :: thesis: for i being Element of Seg d holds
( l . i in G . i & r . i in G . i )
let i be Element of Seg d; :: thesis: ( l . i in G . i & r . i in G . i )
[(l . i),(r . i)] is Gap of G . i by A28;
hence ( l . i in G . i & r . i in G . i ) by Th13; :: thesis: verum
end;
hence ( l in product G & r in product G ) by Th8; :: thesis: ( ( [1,[l,r]] = [0,[l,r]] & A = cell (l,r) ) or ( [1,[l,r]] = [1,[l,r]] & A = cell (l,r) ) )
thus ( ( [1,[l,r]] = [0,[l,r]] & A = cell (l,r) ) or ( [1,[l,r]] = [1,[l,r]] & A = cell (l,r) ) ) by A25; :: thesis: verum
end;
end;
end;
consider f being Function such that
A29: ( dom f = { H2(l,r) where l, r is Element of REAL d : S1[l,r] } & ( for A being object st A in { H2(l,r) where l, r is Element of REAL d : S1[l,r] } holds
S4[A,f . A] ) ) from A30: f is one-to-one
proof
let A, A9 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not A in dom f or not A9 in dom f or not f . A = f . A9 or A = A9 )
assume that
A31: A in dom f and
A32: A9 in dom f and
A33: f . A = f . A9 ; :: thesis: A = A9
consider l, r being Element of REAL d such that
A34: S3[A,l,r,f . A] by ;
consider l9, r9 being Element of REAL d such that
A35: S3[A9,l9,r9,f . A9] by ;
per cases ( ( f . A = [0,[l,r]] & A = cell (l,r) ) or ( f . A = [1,[l,r]] & A = cell (l,r) ) ) by A34;
suppose A36: ( f . A = [0,[l,r]] & A = cell (l,r) ) ; :: thesis: A = A9
then A37: [l,r] = [l9,r9] by ;
then l = l9 by XTUPLE_0:1;
hence A = A9 by ; :: thesis: verum
end;
suppose A38: ( f . A = [1,[l,r]] & A = cell (l,r) ) ; :: thesis: A = A9
then A39: [l,r] = [l9,r9] by ;
then l = l9 by XTUPLE_0:1;
hence A = A9 by ; :: thesis: verum
end;
end;
end;
reconsider X = product G as finite set ;
A40: rng f c= [:{0,1},[:X,X:]:]
proof
let lr be object ; :: according to TARSKI:def 3 :: thesis: ( not lr in rng f or lr in [:{0,1},[:X,X:]:] )
assume lr in rng f ; :: thesis: lr in [:{0,1},[:X,X:]:]
then consider A being object such that
A41: A in dom f and
A42: lr = f . A by FUNCT_1:def 3;
consider l, r being Element of REAL d such that
A43: S3[A,l,r,f . A] by ;
A44: 0 in {0,1} by TARSKI:def 2;
A45: 1 in {0,1} by TARSKI:def 2;
[l,r] in [:X,X:] by ;
hence lr in [:{0,1},[:X,X:]:] by ; :: thesis: verum
end;
{ H2(l,r) where l, r is Element of REAL d : S1[l,r] } c= bool (REAL d) from hence { (cell (l,r)) where l, r is Element of REAL d : ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) } is non empty finite Subset-Family of (REAL d) by ; :: thesis: verum