defpred S₁[ 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 H₂( Element of REAL d, Element of REAL d) -> non empty Subset of (REAL d) = cell $1,$2;
set CELLS = { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } ;
reconsider X = Seg k as Subset of (Seg d) by A1, FINSEQ_1:7;
defpred S₂[ Element of Seg d, Element of [:REAL ,REAL :]] 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

let i be Element of Seg d; :: thesis:
thus ex lri being Element of [:REAL ,REAL :] st S₂[i,lri] :: thesis:

proof

per cases ;

suppose A3: i in X ; :: thesis:

consider li, ri being Real such that
A4: ( li in G . i & ri in G . i & li < ri & ( for xi being Real st xi in G . i & li < xi holds
not xi < ri ) ) by Th14;
take [li,ri] ; :: thesis:
[li,ri] is Gap of G . i by A4, Def6;
hence S₂[i,[li,ri]] by A3, A4; :: thesis:

end;

suppose A5: not i in X ; :: thesis:

consider li being Element of G . i;
reconsider li = li as Real ;
reconsider lri = [li,li] as Element of [:REAL ,REAL :] ;
take lri ; :: thesis:
thus S₂[i,lri] by A5; :: thesis:

end;

consider lr being Function of (Seg d),[:REAL ,REAL :] such that
A6: for i being Element of Seg d holds S₂[i,lr . i] from FUNCT_2:sch 3(A2);
deffunc H₃( Element of Seg d) -> Element of REAL = (lr . $1) `1 ;
consider l being Function of (Seg d),REAL such that
A7: for i being Element of Seg d holds l . i = H₃(i) from FUNCT_2:sch 4();
deffunc H₄( Element of Seg d) -> Element of REAL = (lr . $1) `2 ;
consider r being Function of (Seg d),REAL such that
A8: for i being Element of Seg d holds r . i = H₄(i) from FUNCT_2:sch 4();
reconsider l = l, r = r as Element of REAL d by Def4;

A9: now

let i be Element of Seg d; :: thesis:
( l . i = (lr . i) `1 & r . i = (lr . i) `2 ) by A7, A8;
hence lr . i = [(l . i),(r . i)] by MCART_1:23; :: thesis:

end;

now

take A = cell l,r; :: thesis:
thus A = cell l,r ; :: thesis:

now

take X = X; :: thesis:
thus card X = k by FINSEQ_1:78; :: thesis:
take l = l; :: thesis:
take r = r; :: thesis:
thus A = cell l,r ; :: thesis:
let i be Element of Seg d; :: thesis:

per cases ;

suppose A10: i in X ; :: thesis:

then consider li, ri being Real such that
A11: ( lr . i = [li,ri] & li < ri & lr . i is Gap of G . i ) by A6;
lr . i = [(l . i),(r . i)] by A9;
then ( li = l . i & ri = r . i ) by A11, ZFMISC_1:33;
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 A10, A11; :: thesis:

end;

suppose A12: not i in X ; :: thesis:

then consider li being Real such that
A13: ( lr . i = [li,li] & li in G . i ) by A6;
[li,li] = [(l . i),(r . i)] by A9, A13;
then ( li = l . i & li = r . i ) by ZFMISC_1:33;
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 A12, A13; :: thesis:

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:

end;

then A14: cell l,r in { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } ;
defpred S₃[ set , Element of REAL d, Element of REAL d, set ] 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 S₄[ set , set ] means ex l, r being Element of REAL d st S₃[$1,l,r,$2];
A15: for A being set st A in { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } holds
ex lr being set st S₄[A,lr]

proof

let A be set ; :: thesis:
assume A in { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } ; :: thesis:
then consider l, r being Element of REAL d such that
A16: ( 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 ) ) ) ) ) ;

per cases by A16;

suppose 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:

then consider X being Subset of (Seg d) such that
A17: 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 [0 ,[l,r]] ; :: thesis:
take l ; :: thesis:
take r ; :: thesis:

now

let i be Element of Seg d; :: thesis:
( ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( l . i = r . i & l . i in G . i ) ) by A17;
hence ( l . i in G . i & r . i in G . i ) by Th17; :: thesis:

end;

hence ( l in product G & r in product G ) by Th10; :: thesis:
thus ( ( [0 ,[l,r]] = [0 ,[l,r]] & A = cell l,r ) or ( [0 ,[l,r]] = [1,[l,r]] & A = cell l,r ) ) by A16; :: thesis:

end;

suppose A18: ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis:

take [1,[l,r]] ; :: thesis:
take l ; :: thesis:
take r ; :: thesis:

now

let i be Element of Seg d; :: thesis:
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) by A18;
hence ( l . i in G . i & r . i in G . i ) by Th17; :: thesis:

end;

hence ( l in product G & r in product G ) by Th10; :: thesis:
thus ( ( [1,[l,r]] = [0 ,[l,r]] & A = cell l,r ) or ( [1,[l,r]] = [1,[l,r]] & A = cell l,r ) ) by A16; :: thesis:

end;

consider f being Function such that
A19: ( dom f = { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } & ( for A being set st A in { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } holds
S₄[A,f . A] ) ) from CLASSES1:sch 1(A15);
A20: f is one-to-one

proof

let A, A' be set ; :: according to FUNCT_1:def 8 :: thesis:
assume A21: ( A in dom f & A' in dom f & f . A = f . A' ) ; :: thesis:
then consider l, r being Element of REAL d such that
A22: S₃[A,l,r,f . A] by A19;
consider l', r' being Element of REAL d such that
A23: S₃[A',l',r',f . A'] by A19, A21;

per cases by A22;

suppose A24: ( f . A = [0 ,[l,r]] & A = cell l,r ) ; :: thesis:

then [l,r] = [l',r'] by A21, A23, ZFMISC_1:33;
then ( l = l' & r = r' ) by ZFMISC_1:33;
hence A = A' by A23, A24; :: thesis:

end;

suppose A25: ( f . A = [1,[l,r]] & A = cell l,r ) ; :: thesis:

then [l,r] = [l',r'] by A21, A23, ZFMISC_1:33;
then ( l = l' & r = r' ) by ZFMISC_1:33;
hence A = A' by A23, A25; :: thesis:

end;

reconsider X = product G as finite set by Th11;
rng f c= [:{0 ,1},[:X,X:]:]

proof

let lr be set ; :: according to TARSKI:def 3 :: thesis:
assume lr in rng f ; :: thesis:
then consider A being set such that
A26: ( A in dom f & lr = f . A ) by FUNCT_1:def 5;
consider l, r being Element of REAL d such that
A27: S₃[A,l,r,f . A] by A19, A26;
( 0 in {0 ,1} & 1 in {0 ,1} & [l,r] in [:X,X:] ) by A27, TARSKI:def 2, ZFMISC_1:106;
hence lr in [:{0 ,1},[:X,X:]:] by A26, A27, ZFMISC_1:106; :: thesis:

end;

then A28: rng f is finite ;
{ H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } c= bool (REAL d) from CHAIN_1:sch 1();
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 A14, A19, A20, A28, CARD_1:97; :: thesis: