let f be FinSequence of (); :: thesis: for q being Point of () st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds
(L~ (f -: q)) /\ (L~ (f :- q)) = {q}

let q be Point of (); :: thesis: ( q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. implies (L~ (f -: q)) /\ (L~ (f :- q)) = {q} )
assume that
A1: q in rng f and
A2: 1 <> q .. f and
A3: q .. f <> len f and
A4: f is unfolded and
A5: f is s.n.c. ; :: thesis: (L~ (f -: q)) /\ (L~ (f :- q)) = {q}
A6: (f :- q) /. 1 = q by FINSEQ_5:53;
q .. f <= len f by ;
then q .. f < len f by ;
then (q .. f) + 1 <= len f by NAT_1:13;
then A7: 1 <= (len f) - (q .. f) by XREAL_1:19;
len (f :- q) = ((len f) - (q .. f)) + 1 by ;
then 1 + 1 <= len (f :- q) by ;
then A8: rng (f :- q) c= L~ (f :- q) by Th18;
1 in dom (f :- q) by FINSEQ_5:6;
then A9: q in rng (f :- q) by ;
not f -: q is empty by ;
then A10: len (f -: q) in dom (f -: q) by FINSEQ_5:6;
A11: len (f -: q) = q .. f by ;
thus (L~ (f -: q)) /\ (L~ (f :- q)) c= {q} :: according to XBOOLE_0:def 10 :: thesis: {q} c= (L~ (f -: q)) /\ (L~ (f :- q))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ (f -: q)) /\ (L~ (f :- q)) or x in {q} )
assume A12: x in (L~ (f -: q)) /\ (L~ (f :- q)) ; :: thesis: x in {q}
then reconsider p = x as Point of () ;
p in L~ (f -: q) by ;
then consider i being Nat such that
A13: 1 <= i and
A14: i + 1 <= len (f -: q) and
A15: p in LSeg ((f -: q),i) by Th13;
A16: LSeg ((f -: q),i) = LSeg (f,i) by ;
p in L~ (f :- q) by ;
then consider j being Nat such that
A17: 1 <= j and
j + 1 <= len (f :- q) and
A18: p in LSeg ((f :- q),j) by Th13;
consider j9 being Nat such that
A19: j = j9 + 1 by ;
reconsider j9 = j9 as Element of NAT by ORDINAL1:def 12;
A20: LSeg ((f :- q),j) = LSeg (f,(j9 + (q .. f))) by ;
per cases ( ( i + 1 = len (f -: q) & j9 = 0 ) or ( i + 1 = len (f -: q) & j9 <> 0 ) or i + 1 <> len (f -: q) ) ;
suppose that A21: i + 1 = len (f -: q) and
A22: j9 = 0 ; :: thesis: x in {q}
q .. f <= len f by ;
then q .. f < len f by ;
then (i + 1) + 1 <= len f by ;
then i + (1 + 1) <= len f ;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {(f /. (q .. f))} by A4, A11, A13, A16, A20, A21, A22
.= {q} by ;
hence x in {q} by ; :: thesis: verum
end;
suppose that A23: i + 1 = len (f -: q) and
A24: j9 <> 0 ; :: thesis: x in {q}
1 <= j9 by ;
then (i + 1) + 1 <= j9 + (q .. f) by ;
then i + 1 < j9 + (q .. f) by NAT_1:13;
then LSeg ((f -: q),i) misses LSeg ((f :- q),j) by A5, A16, A20;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {} ;
hence x in {q} by ; :: thesis: verum
end;
suppose A25: i + 1 <> len (f -: q) ; :: thesis: x in {q}
A26: q .. f <= j9 + (q .. f) by NAT_1:11;
i + 1 < q .. f by ;
then i + 1 < j9 + (q .. f) by ;
then LSeg ((f -: q),i) misses LSeg ((f :- q),j) by A5, A16, A20;
then (LSeg ((f -: q),i)) /\ (LSeg ((f :- q),j)) = {} ;
hence x in {q} by ; :: thesis: verum
end;
end;
end;
1 <= q .. f by ;
then 1 < q .. f by ;
then 1 + 1 <= q .. f by NAT_1:13;
then A27: rng (f -: q) c= L~ (f -: q) by ;
(f -: q) /. (q .. f) = q by ;
then q in rng (f -: q) by ;
then q in (L~ (f -: q)) /\ (L~ (f :- q)) by ;
hence {q} c= (L~ (f -: q)) /\ (L~ (f :- q)) by ZFMISC_1:31; :: thesis: verum