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

( 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

thus
( l = l9 & r = r9 implies cell (l,r) = cell (l9,r9) )
; :: thesis: verum
assume A2:
cell (l,r) = cell (l9,r9)
; :: thesis: ( l = l9 & r = r9 )

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

end;

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;

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

now :: thesis: for i being Element of Seg d holds r . i = r9 . i

hence
( l = l9 & r = r9 )
by A5, FUNCT_2:63; :: thesis: verumlet 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;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

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;

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

now :: thesis: for i being Element of Seg d holds r . i = r9 . i

hence
( l = l9 & r = r9 )
by A10, FUNCT_2:63; :: thesis: verumlet 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;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