let d9 be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ) )
A8: now :: thesis: for i being Element of Seg d holds
( i in X iff i <> i0 )
let i be Element of Seg d; :: thesis: ( i in X iff i <> i0 )
( i in (Seg d) \ X iff i = i0 ) by A7, TARSKI:def 1;
hence ( i in X iff i <> i0 ) by XBOOLE_0:def 5; :: thesis: verum
end;
thus A = cell (l,r) by A3; :: thesis: ( 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; :: thesis: 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; :: thesis: ( i <> i0 implies ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) )
assume i <> i0 ; :: thesis: ( 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; :: thesis: 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 ) ; :: thesis: 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 ) ) ) )
proof
thus card X = (card (Seg d)) - (card {i0}) by CARD_2:44
.= d - (card {i0}) by FINSEQ_1:57
.= d - 1 by CARD_1:30
.= d9 by A1 ; :: thesis: 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 ) )
let i be Element of Seg d; :: thesis: ( ( 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 ) )
( i in {i0} iff i = i0 ) by TARSKI:def 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 A10, A11, A12, XBOOLE_0:def 5; :: thesis: verum
end;
hence A in cells (d9,G) by A2, A9, Th29; :: thesis: verum