let d be non zero Element of NAT ; :: thesis: for l, r, l', r' 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 l',r' iff ( l = l' & r = r' ) )
let l, r, l', r' 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 l',r' iff ( l = l' & r = r' ) ) )
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 l',r' iff ( l = l' & r = r' ) )
thus ( cell l,r = cell l',r' implies ( l = l' & r = r' ) ) :: thesis: ( l = l' & r = r' implies cell l,r = cell l',r' )

proof

assume A2: cell l,r = cell l',r' ; :: thesis: ( l = l' & r = r' )

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 = l' & r = r' )

then A4: for i being Element of Seg d holds
( l . i <= l' . i & l' . i <= r' . i & r' . i <= r . i ) by A2, Th29;
reconsider l = l, r = r, l' = l', r' = r' as Function of Seg d, REAL by Def4;

A5: now

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

end;

now

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

end;

hence ( l = l' & r = r' ) by A5, FUNCT_2:113; :: thesis: verum

end;

suppose A8: for i being Element of Seg d holds l . i > r . i ; :: thesis: ( l = l' & r = r' )

then A9: for i being Element of Seg d holds
( r . i <= r' . i & r' . i < l' . i & l' . i <= l . i ) by A2, Th30;
reconsider l = l, r = r, l' = l', r' = r' as Function of Seg d, REAL by Def4;

A10: now

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

end;

now

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

end;

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

end;

end;

end;

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