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:5;
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 ) ) );

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:
[li,ri] is Gap of G . i by A4, A5, A6, A7, Def5;
hence S₂[i,[li,ri]] by A3, A6; :: thesis:

end;

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 [:REAL,REAL:] ;
take lri ; :: thesis:
thus S₂[i,lri] by A8; :: thesis:

end;

consider lr being Function of (Seg d),[:REAL,REAL:] such that
A9: 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
A10: 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
A11: 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 Def3;

A12: now :: thesis:

let i be Element of Seg d; :: thesis:
A13: l . i = (lr . i) `1 by A10;
r . i = (lr . i) `2 by A11;
hence lr . i = [(l . i),(r . i)] by A13, MCART_1:21; :: thesis:

end;

now :: thesis:

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

now :: thesis:

take X = X; :: thesis:
thus card X = k by FINSEQ_1:57; :: 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 A14: i in X ; :: thesis:

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 A15, 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 A14, A15, A16, A17, A18, XTUPLE_0:1; :: thesis:

end;

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

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 A12, A20;
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 A19, A21, A22, XTUPLE_0:1; :: 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 A23: cell (l,r) in { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } ;
defpred S₃[ 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 S₄[ object , object ] means ex l, r being Element of REAL d st S₃[$1,l,r,$2];
A24: for A being object st A in { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } holds
ex lr being object st S₄[A,lr]

proof

let A be object ; :: 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
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 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:

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

now :: thesis:

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 A27;
hence ( l . i in G . i & r . i in G . i ) by Th13; :: thesis:

end;

hence ( l in product G & r in product G ) by Th8; :: thesis:
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:

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:

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

now :: thesis:

let i be Element of Seg d; :: thesis:
[(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:

end;

hence ( l in product G & r in product G ) by Th8; :: thesis:
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:

end;

consider f being Function such that
A29: ( dom f = { H₂(l,r) where l, r is Element of REAL d : S₁[l,r] } & ( for A being object 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(A24);
A30: f is one-to-one

proof

let A, A9 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A31: A in dom f and
A32: A9 in dom f and
A33: f . A = f . A9 ; :: thesis:
consider l, r being Element of REAL d such that
A34: S₃[A,l,r,f . A] by A29, A31;
consider l9, r9 being Element of REAL d such that
A35: S₃[A9,l9,r9,f . A9] by A29, A32;

per cases by A34;

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

then A37: [l,r] = [l9,r9] by A33, A35, XTUPLE_0:1;
then l = l9 by XTUPLE_0:1;
hence A = A9 by A35, A36, A37, XTUPLE_0:1; :: thesis:

end;

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

then A39: [l,r] = [l9,r9] by A33, A35, XTUPLE_0:1;
then l = l9 by XTUPLE_0:1;
hence A = A9 by A35, A38, A39, XTUPLE_0:1; :: thesis:

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:
assume lr in rng f ; :: thesis:
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: S₃[A,l,r,f . A] by A29, A41;
A44: 0 in {0,1} by TARSKI:def 2;
A45: 1 in {0,1} by TARSKI:def 2;
[l,r] in [:X,X:] by A43, ZFMISC_1:87;
hence lr in [:{0,1},[:X,X:]:] by A42, A43, A44, A45, ZFMISC_1:87; :: thesis:

end;

{ 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 A23, A29, A30, A40, CARD_1:59; :: thesis: