let x0 be Real; :: thesis:
let seq be Real_Sequence; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
assume A1: ( rng seq c= (dom f) /\ (left_open_halfline x0) or rng seq c= (dom f) /\ (right_open_halfline x0) ) ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in rng seq ; :: thesis:
then consider n being Element of NAT such that
A3: seq . n = x by FUNCT_2:113;

per cases by A1;

suppose A4: rng seq c= (dom f) /\ (left_open_halfline x0) ; :: thesis:

then seq . n in left_open_halfline x0 by A2, A3, XBOOLE_0:def 4;
then seq . n in { g1 where g1 is Real : g1 < x0 } by XXREAL_1:229;
then ex g1 being Real st
( g1 = seq . n & g1 < x0 ) ;
then A5: not x in {x0} by A3, TARSKI:def 1;
seq . n in dom f by A2, A3, A4, XBOOLE_0:def 4;
hence x in (dom f) \ {x0} by A3, A5, XBOOLE_0:def 5; :: thesis:

end;

suppose A6: rng seq c= (dom f) /\ (right_open_halfline x0) ; :: thesis:

then seq . n in right_open_halfline x0 by A2, A3, XBOOLE_0:def 4;
then seq . n in { g1 where g1 is Real : x0 < g1 } by XXREAL_1:230;
then ex g1 being Real st
( g1 = seq . n & x0 < g1 ) ;
then A7: not x in {x0} by A3, TARSKI:def 1;
seq . n in dom f by A2, A3, A6, XBOOLE_0:def 4;
hence x in (dom f) \ {x0} by A3, A7, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

hence x in (dom f) \ {x0} ; :: thesis: