let d9 be Nat; for d being non zero Nat
for G being Grating of d st d = d9 + 1 holds
for A being Subset of (REAL d) holds
( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
let d be non zero Nat; for G being Grating of d st d = d9 + 1 holds
for A being Subset of (REAL d) holds
( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
let G be Grating of d; ( d = d9 + 1 implies for A being Subset of (REAL d) holds
( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )
assume A1:
d = d9 + 1
; for A being Subset of (REAL d) holds
( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
then A2:
d9 < d
by NAT_1:13;
let A be Subset of (REAL d); ( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
hereby ( ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) implies A in cells (d9,G) )
assume
A in cells (
d9,
G)
;
ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )then consider l,
r being
Element of
REAL d such that A3:
A = cell (
l,
r)
and A4:
( ex
X being
Subset of
(Seg d) st
(
card X = d9 & ( 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 (
d9 = d & ( for
i being
Element of
Seg d holds
(
r . i < l . i &
[(l . i),(r . i)] is
Gap of
G . i ) ) ) )
by A2, Th29;
take l =
l;
ex r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )take r =
r;
ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )consider X being
Subset of
(Seg d) such that A5:
card X = d9
and A6:
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 ) )
by A1, A4;
card ((Seg d) \ X) =
(card (Seg d)) - (card X)
by CARD_2:44
.=
d - d9
by A5, FINSEQ_1:57
.=
1
by A1
;
then consider i0 being
object such that A7:
(Seg d) \ X = {i0}
by CARD_2:42;
i0 in (Seg d) \ X
by A7, TARSKI:def 1;
then reconsider i0 =
i0 as
Element of
Seg d by XBOOLE_0:def 5;
take i0 =
i0;
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )thus
A = cell (
l,
r)
by A3;
( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )
not
i0 in X
by A8;
hence
(
l . i0 = r . i0 &
l . i0 in G . i0 )
by A6;
for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )let i be
Element of
Seg d;
( i <> i0 implies ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) )assume
i <> i0
;
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )then
i in X
by A8;
hence
(
l . i < r . i &
[(l . i),(r . i)] is
Gap of
G . i )
by A6;
verum
end;
given l, r being Element of REAL d, i0 being Element of Seg d such that A9:
A = cell (l,r)
and
A10:
l . i0 = r . i0
and
A11:
l . i0 in G . i0
and
A12:
for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )
; A in cells (d9,G)
reconsider X = (Seg d) \ {i0} as Subset of (Seg d) by XBOOLE_1:36;
( card X = d9 & ( 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
A in cells (d9,G)
by A2, A9, Th29; verum