defpred S_{1}[ 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_{2}( Element of REAL d, Element of REAL d) -> non empty Subset of (REAL d) = cell ($1,$2);

set CELLS = { H_{2}(l,r) where l, r is Element of REAL d : S_{1}[l,r] } ;

reconsider X = Seg k as Subset of (Seg d) by A1, FINSEQ_1:5;

defpred S_{2}[ 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 ) ) );

A9: for i being Element of Seg d holds S_{2}[i,lr . i]
from FUNCT_2:sch 3(A2);

deffunc H_{3}( 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_{3}(i)
from FUNCT_2:sch 4();

deffunc H_{4}( 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_{4}(i)
from FUNCT_2:sch 4();

reconsider l = l, r = r as Element of REAL d by Def3;

_{2}(l,r) where l, r is Element of REAL d : S_{1}[l,r] }
;

defpred S_{3}[ 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_{4}[ object , object ] means ex l, r being Element of REAL d st S_{3}[$1,l,r,$2];

A24: for A being object st A in { H_{2}(l,r) where l, r is Element of REAL d : S_{1}[l,r] } holds

ex lr being object st S_{4}[A,lr]

A29: ( dom f = { H_{2}(l,r) where l, r is Element of REAL d : S_{1}[l,r] } & ( for A being object st A in { H_{2}(l,r) where l, r is Element of REAL d : S_{1}[l,r] } holds

S_{4}[A,f . A] ) )
from CLASSES1:sch 1(A24);

A30: f is one-to-one

A40: rng f c= [:{0,1},[:X,X:]:]_{2}(l,r) where l, r is Element of REAL d : S_{1}[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: verum

( 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

set CELLS = { H

reconsider X = Seg k as Subset of (Seg d) by A1, FINSEQ_1:5;

defpred S

( $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 [:REAL,REAL:] st S_{2}[i,lri]

consider lr being Function of (Seg d),[:REAL,REAL:] such that let i be Element of Seg d; :: thesis: ex lri being Element of [:REAL,REAL:] st S_{2}[i,lri]

thus ex lri being Element of [:REAL,REAL:] st S_{2}[i,lri]
:: thesis: verum

end;thus ex lri being Element of [:REAL,REAL:] st S

proof
end;

per cases
( i in X or not i in X )
;

end;

suppose A3:
i in X
; :: thesis: ex lri being Element of [:REAL,REAL:] st S_{2}[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: S_{2}[i,[li,ri]]

[li,ri] is Gap of G . i by A4, A5, A6, A7, Def5;

hence S_{2}[i,[li,ri]]
by A3, A6; :: thesis: verum

end;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: S

[li,ri] is Gap of G . i by A4, A5, A6, A7, Def5;

hence S

suppose A8:
not i in X
; :: thesis: ex lri being Element of [:REAL,REAL:] st S_{2}[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 [:REAL,REAL:] ;

take lri ; :: thesis: S_{2}[i,lri]

thus S_{2}[i,lri]
by A8; :: thesis: verum

end;reconsider li = the Element of G . i as Element of REAL ;

reconsider lri = [li,li] as Element of [:REAL,REAL:] ;

take lri ; :: thesis: S

thus S

A9: for i being Element of Seg d holds S

deffunc H

consider l being Function of (Seg d),REAL such that

A10: for i being Element of Seg d holds l . i = H

deffunc H

consider r being Function of (Seg d),REAL such that

A11: for i being Element of Seg d holds r . i = H

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 A13, MCART_1:21; :: thesis: verum

end;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: verum

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 ) ) ) ) ) )

then A23:
cell (l,r) in { H( 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 ) ) ) ) )

( 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;( 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 ) ) ) ) )

hence
ex l, r being Element of REAL 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

( ( b_{7} in b_{4} & b_{5} . b_{7} < b_{6} . b_{7} & [(b_{5} . b_{7}),(b_{6} . b_{7})] is Gap of G . b_{7} ) or ( not b_{7} in b_{4} & b_{5} . b_{7} = b_{6} . b_{7} & b_{5} . b_{7} in G . b_{7} ) ) ) ) )

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

( ( b_{7} in b_{4} & b_{5} . b_{7} < b_{6} . b_{7} & [(b_{5} . b_{7}),(b_{6} . b_{7})] is Gap of G . b_{7} ) or ( not b_{7} in b_{4} & b_{5} . b_{7} = b_{6} . b_{7} & b_{5} . b_{7} in G . b_{7} ) ) ) )

take l = l; :: thesis: ex r being Element of REAL d st

( A = cell (l,r) & ( for i being Element of Seg d holds

( ( b_{6} in b_{3} & b_{4} . b_{6} < b_{5} . b_{6} & [(b_{4} . b_{6}),(b_{5} . b_{6})] is Gap of G . b_{6} ) or ( not b_{6} in b_{3} & b_{4} . b_{6} = b_{5} . b_{6} & b_{4} . b_{6} in G . b_{6} ) ) ) )

take r = r; :: thesis: ( A = cell (l,r) & ( for i being Element of Seg d holds

( ( b_{5} in b_{2} & b_{3} . b_{5} < b_{4} . b_{5} & [(b_{3} . b_{5}),(b_{4} . b_{5})] is Gap of G . b_{5} ) or ( not b_{5} in b_{2} & b_{3} . b_{5} = b_{4} . b_{5} & b_{3} . b_{5} in G . b_{5} ) ) ) )

thus A = cell (l,r) ; :: thesis: for i being Element of Seg d holds

( ( b_{5} in b_{2} & b_{3} . b_{5} < b_{4} . b_{5} & [(b_{3} . b_{5}),(b_{4} . b_{5})] is Gap of G . b_{5} ) or ( not b_{5} in b_{2} & b_{3} . b_{5} = b_{4} . b_{5} & b_{3} . b_{5} in G . b_{5} ) )

let i be Element of Seg d; :: thesis: ( ( b_{4} in b_{1} & b_{2} . b_{4} < b_{3} . b_{4} & [(b_{2} . b_{4}),(b_{3} . b_{4})] is Gap of G . b_{4} ) or ( not b_{4} in b_{1} & b_{2} . b_{4} = b_{3} . b_{4} & b_{2} . b_{4} in G . b_{4} ) )

end;( A = cell (l,r) & ( for i being Element of Seg d holds

( ( b

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

( ( b

take l = l; :: thesis: ex r being Element of REAL d st

( A = cell (l,r) & ( for i being Element of Seg d holds

( ( b

take r = r; :: thesis: ( A = cell (l,r) & ( for i being Element of Seg d holds

( ( b

thus A = cell (l,r) ; :: thesis: for i being Element of Seg d holds

( ( b

let i be Element of Seg d; :: thesis: ( ( b

per cases
( i in X or not i in X )
;

end;

suppose A14:
i in X
; :: thesis: ( ( b_{4} in b_{1} & b_{2} . b_{4} < b_{3} . b_{4} & [(b_{2} . b_{4}),(b_{3} . b_{4})] is Gap of G . b_{4} ) or ( not b_{4} in b_{1} & b_{2} . b_{4} = b_{3} . b_{4} & b_{2} . b_{4} in G . b_{4} ) )

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

end;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: verum

suppose A19:
not i in X
; :: thesis: ( ( b_{4} in b_{1} & b_{2} . b_{4} < b_{3} . b_{4} & [(b_{2} . b_{4}),(b_{3} . b_{4})] is Gap of G . b_{4} ) or ( not b_{4} in b_{1} & b_{2} . b_{4} = b_{3} . b_{4} & b_{2} . b_{4} in G . b_{4} ) )

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

end;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: verum

( 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

defpred S

defpred S

A24: for A being object st A in { H

ex lr being object st S

proof

consider f being Function such that
let A be object ; :: thesis: ( A in { H_{2}(l,r) where l, r is Element of REAL d : S_{1}[l,r] } implies ex lr being object st S_{4}[A,lr] )

assume A in { H_{2}(l,r) where l, r is Element of REAL d : S_{1}[l,r] }
; :: thesis: ex lr being object st S_{4}[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 ) ) ) ) ;

end;assume A in { H

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;

end;

( 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 S_{4}[A,lr]

( 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 S

take
[0,[l,r]]
; :: thesis: S_{4}[A,[0,[l,r]]]

take l ; :: thesis: ex r being Element of REAL d st S_{3}[A,l,r,[0,[l,r]]]

take r ; :: thesis: S_{3}[A,l,r,[0,[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;take l ; :: thesis: ex r being Element of REAL d st S

take r ; :: thesis: S

now :: thesis: for i being Element of Seg d holds

( l . i in G . i & r . i in G . i )

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) ) )( 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;( ( 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

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

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 S_{4}[A,lr]

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: ex lr being object st S

take
[1,[l,r]]
; :: thesis: S_{4}[A,[1,[l,r]]]

take l ; :: thesis: ex r being Element of REAL d st S_{3}[A,l,r,[1,[l,r]]]

take r ; :: thesis: S_{3}[A,l,r,[1,[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;take l ; :: thesis: ex r being Element of REAL d st S

take r ; :: thesis: S

now :: thesis: for i being Element of Seg d holds

( l . i in G . i & r . i in G . i )

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) ) )( 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;[(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

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

A29: ( dom f = { H

S

A30: f is one-to-one

proof

reconsider X = product G as finite set ;
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: S_{3}[A,l,r,f . A]
by A29, A31;

consider l9, r9 being Element of REAL d such that

A35: S_{3}[A9,l9,r9,f . A9]
by A29, A32;

end;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: S

consider l9, r9 being Element of REAL d such that

A35: S

per cases
( ( f . A = [0,[l,r]] & A = cell (l,r) ) or ( f . A = [1,[l,r]] & A = cell (l,r) ) )
by A34;

end;

A40: rng f c= [:{0,1},[:X,X:]:]

proof

{ H
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: S_{3}[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: verum

end;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: S

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

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