let d be non zero Nat; :: thesis: for l, r, l9, r9 being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i or for i being Element of Seg d holds l . i > r . i ) holds
( cell (l,r) = cell (l9,r9) iff ( l = l9 & r = r9 ) )
let l, r, l9, r9 be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l . i <= r . i or for i being Element of Seg d holds l . i > r . i ) implies ( cell (l,r) = cell (l9,r9) iff ( l = l9 & r = r9 ) ) )
assume A1: ( for i being Element of Seg d holds l . i <= r . i or for i being Element of Seg d holds l . i > r . i ) ; :: thesis: ( cell (l,r) = cell (l9,r9) iff ( l = l9 & r = r9 ) )
thus ( cell (l,r) = cell (l9,r9) implies ( l = l9 & r = r9 ) ) :: thesis: ( l = l9 & r = r9 implies cell (l,r) = cell (l9,r9) )
proof
assume A2: cell (l,r) = cell (l9,r9) ; :: thesis: ( l = l9 & r = r9 )
per cases ( for i being Element of Seg d holds l . i <= r . i or for i being Element of Seg d holds l . i > r . i ) by A1;
suppose A3: for i being Element of Seg d holds l . i <= r . i ; :: thesis: ( l = l9 & r = r9 )
then A4: for i being Element of Seg d holds
( l . i <= l9 . i & l9 . i <= r9 . i & r9 . i <= r . i ) by A2, Th25;
reconsider l = l, r = r, l9 = l9, r9 = r9 as Function of (Seg d),REAL by Def3;
A5: now :: thesis: for i being Element of Seg d holds l . i = l9 . i
let i be Element of Seg d; :: thesis: l . i = l9 . i
A6: l . i <= l9 . i by A2, A3, Th25;
l9 . i <= l . i by A2, A4, Th25;
hence l . i = l9 . i by A6, XXREAL_0:1; :: thesis: verum
end;
now :: thesis: for i being Element of Seg d holds r . i = r9 . i
let i be Element of Seg d; :: thesis: r . i = r9 . i
A7: r . i <= r9 . i by A2, A4, Th25;
r9 . i <= r . i by A2, A3, Th25;
hence r . i = r9 . i by A7, XXREAL_0:1; :: thesis: verum
end;
hence ( l = l9 & r = r9 ) by A5, FUNCT_2:63; :: thesis: verum
end;
suppose A8: for i being Element of Seg d holds l . i > r . i ; :: thesis: ( l = l9 & r = r9 )
then A9: for i being Element of Seg d holds
( r . i <= r9 . i & r9 . i < l9 . i & l9 . i <= l . i ) by A2, Th26;
reconsider l = l, r = r, l9 = l9, r9 = r9 as Function of (Seg d),REAL by Def3;
A10: now :: thesis: for i being Element of Seg d holds l . i = l9 . i
let i be Element of Seg d; :: thesis: l . i = l9 . i
A11: l . i <= l9 . i by A2, A9, Th26;
l9 . i <= l . i by A2, A8, Th26;
hence l . i = l9 . i by A11, XXREAL_0:1; :: thesis: verum
end;
now :: thesis: for i being Element of Seg d holds r . i = r9 . i
let i be Element of Seg d; :: thesis: r . i = r9 . i
A12: r . i <= r9 . i by A2, A8, Th26;
r9 . i <= r . i by A2, A9, Th26;
hence r . i = r9 . i by A12, XXREAL_0:1; :: thesis: verum
end;
hence ( l = l9 & r = r9 ) by A10, FUNCT_2:63; :: thesis: verum
end;
end;
end;
thus ( l = l9 & r = r9 implies cell (l,r) = cell (l9,r9) ) ; :: thesis: verum