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 set ; :: 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:190;

now

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

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

then A4: ( seq . n in dom f & 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 not x in {x0} by A3, TARSKI:def 1;
hence x in (dom f) \ {x0} by A3, A4, XBOOLE_0:def 5; :: thesis: verum

end;

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

then A5: ( seq . n in dom f & 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 not x in {x0} by A3, TARSKI:def 1;
hence x in (dom f) \ {x0} by A3, A5, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

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