let d be non zero Element of 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, Th29;
reconsider l = l, r = r, l9 = l9, r9 = r9 as Function of (Seg d),REAL by Def4;

A5: now

let i be Element of Seg d; :: thesis: l . i = l9 . i
A6: l . i <= l9 . i by A2, A3, Th29;
l9 . i <= l . i by A2, A4, Th29;
hence l . i = l9 . i by A6, XXREAL_0:1; :: thesis: verum

end;

now

let i be Element of Seg d; :: thesis: r . i = r9 . i
A7: r . i <= r9 . i by A2, A4, Th29;
r9 . i <= r . i by A2, A3, Th29;
hence r . i = r9 . i by A7, XXREAL_0:1; :: thesis: verum

end;

hence ( l = l9 & r = r9 ) by A5, FUNCT_2:113; :: 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, Th30;
reconsider l = l, r = r, l9 = l9, r9 = r9 as Function of (Seg d),REAL by Def4;

A10: now

let i be Element of Seg d; :: thesis: l . i = l9 . i
A11: l . i <= l9 . i by A2, A9, Th30;
l9 . i <= l . i by A2, A8, Th30;
hence l . i = l9 . i by A11, XXREAL_0:1; :: thesis: verum

end;

now

let i be Element of Seg d; :: thesis: r . i = r9 . i
A12: r . i <= r9 . i by A2, A8, Th30;
r9 . i <= r . i by A2, A9, Th30;
hence r . i = r9 . i by A12, XXREAL_0:1; :: thesis: verum

end;

hence ( l = l9 & r = r9 ) by A10, FUNCT_2:113; :: thesis: verum

end;

end;

end;

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