let f be FinSequence of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 A1, FINSEQ_4:21;

then q .. f < len f by A3, XXREAL_0:1;

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 A1, FINSEQ_5:50;

then 1 + 1 <= len (f :- q) by A7, XREAL_1:6;

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 A6, PARTFUN2:2;

not f -: q is empty by A1, FINSEQ_5:47;

then A10: len (f -: q) in dom (f -: q) by FINSEQ_5:6;

A11: len (f -: q) = q .. f by A1, FINSEQ_5:42;

thus (L~ (f -: q)) /\ (L~ (f :- q)) c= {q} :: according to XBOOLE_0:def 10 :: thesis: {q} c= (L~ (f -: q)) /\ (L~ (f :- q))

then 1 < q .. f by A2, XXREAL_0:1;

then 1 + 1 <= q .. f by NAT_1:13;

then A27: rng (f -: q) c= L~ (f -: q) by A11, Th18;

(f -: q) /. (q .. f) = q by A1, FINSEQ_5:45;

then q in rng (f -: q) by A11, A10, PARTFUN2:2;

then q in (L~ (f -: q)) /\ (L~ (f :- q)) by A27, A9, A8, XBOOLE_0:def 4;

hence {q} c= (L~ (f -: q)) /\ (L~ (f :- q)) by ZFMISC_1:31; :: thesis: verum

(L~ (f -: q)) /\ (L~ (f :- q)) = {q}

let q be Point of (TOP-REAL 2); :: 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 A1, FINSEQ_4:21;

then q .. f < len f by A3, XXREAL_0:1;

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 A1, FINSEQ_5:50;

then 1 + 1 <= len (f :- q) by A7, XREAL_1:6;

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 A6, PARTFUN2:2;

not f -: q is empty by A1, FINSEQ_5:47;

then A10: len (f -: q) in dom (f -: q) by FINSEQ_5:6;

A11: len (f -: q) = q .. f by A1, FINSEQ_5:42;

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

1 <= q .. f
by A1, FINSEQ_4:21;
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 (TOP-REAL 2) ;

p in L~ (f -: q) by A12, XBOOLE_0:def 4;

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 A14, Th9;

p in L~ (f :- q) by A12, XBOOLE_0:def 4;

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 A17, NAT_1:6;

reconsider j9 = j9 as Element of NAT by ORDINAL1:def 12;

A20: LSeg ((f :- q),j) = LSeg (f,(j9 + (q .. f))) by A1, A19, Th10;

end;assume A12: x in (L~ (f -: q)) /\ (L~ (f :- q)) ; :: thesis: x in {q}

then reconsider p = x as Point of (TOP-REAL 2) ;

p in L~ (f -: q) by A12, XBOOLE_0:def 4;

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 A14, Th9;

p in L~ (f :- q) by A12, XBOOLE_0:def 4;

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 A17, NAT_1:6;

reconsider j9 = j9 as Element of NAT by ORDINAL1:def 12;

A20: LSeg ((f :- q),j) = LSeg (f,(j9 + (q .. f))) by A1, A19, Th10;

per cases
( ( i + 1 = len (f -: q) & j9 = 0 ) or ( i + 1 = len (f -: q) & j9 <> 0 ) or i + 1 <> len (f -: q) )
;

end;

suppose that A21:
i + 1 = len (f -: q)
and

A22: j9 = 0 ; :: thesis: x in {q}

A22: j9 = 0 ; :: thesis: x in {q}

q .. f <= len f
by A1, FINSEQ_4:21;

then q .. f < len f by A3, XXREAL_0:1;

then (i + 1) + 1 <= len f by A11, A21, NAT_1:13;

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 A1, FINSEQ_5:38 ;

hence x in {q} by A15, A18, XBOOLE_0:def 4; :: thesis: verum

end;then q .. f < len f by A3, XXREAL_0:1;

then (i + 1) + 1 <= len f by A11, A21, NAT_1:13;

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 A1, FINSEQ_5:38 ;

hence x in {q} by A15, A18, XBOOLE_0:def 4; :: thesis: verum

suppose that A23:
i + 1 = len (f -: q)
and

A24: j9 <> 0 ; :: thesis: x in {q}

A24: j9 <> 0 ; :: thesis: x in {q}

1 <= j9
by A24, NAT_1:14;

then (i + 1) + 1 <= j9 + (q .. f) by A11, A23, XREAL_1:7;

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 A15, A18, XBOOLE_0:def 4; :: thesis: verum

end;then (i + 1) + 1 <= j9 + (q .. f) by A11, A23, XREAL_1:7;

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 A15, A18, XBOOLE_0:def 4; :: thesis: verum

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 A11, A14, A25, XXREAL_0:1;

then i + 1 < j9 + (q .. f) by A26, XXREAL_0:2;

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 A15, A18, XBOOLE_0:def 4; :: thesis: verum

end;i + 1 < q .. f by A11, A14, A25, XXREAL_0:1;

then i + 1 < j9 + (q .. f) by A26, XXREAL_0:2;

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 A15, A18, XBOOLE_0:def 4; :: thesis: verum

then 1 < q .. f by A2, XXREAL_0:1;

then 1 + 1 <= q .. f by NAT_1:13;

then A27: rng (f -: q) c= L~ (f -: q) by A11, Th18;

(f -: q) /. (q .. f) = q by A1, FINSEQ_5:45;

then q in rng (f -: q) by A11, A10, PARTFUN2:2;

then q in (L~ (f -: q)) /\ (L~ (f :- q)) by A27, A9, A8, XBOOLE_0:def 4;

hence {q} c= (L~ (f -: q)) /\ (L~ (f :- q)) by ZFMISC_1:31; :: thesis: verum