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

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

per cases ( rng seq c= (dom f) /\ (left_open_halfline x0) or rng seq c= (dom f) /\ (right_open_halfline x0) ) by A1;

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

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: verum

end;

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

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: verum

end;

end;

end;

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