let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in rng f holds

L~ (f :- p) c= L~ f

let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies L~ (f :- p) c= L~ f )

assume p in rng f ; :: thesis: L~ (f :- p) c= L~ f

then L~ f = (L~ (f -: p)) \/ (L~ (f :- p)) by Th24;

hence L~ (f :- p) c= L~ f by XBOOLE_1:7; :: thesis: verum

L~ (f :- p) c= L~ f

let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies L~ (f :- p) c= L~ f )

assume p in rng f ; :: thesis: L~ (f :- p) c= L~ f

then L~ f = (L~ (f -: p)) \/ (L~ (f :- p)) by Th24;

hence L~ (f :- p) c= L~ f by XBOOLE_1:7; :: thesis: verum