let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q being Point of (TOP-REAL 2)

for f1, f2 being S-Sequence_in_R2 st p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 holds

ex g1, g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

let p1, p2, q be Point of (TOP-REAL 2); :: thesis: for f1, f2 being S-Sequence_in_R2 st p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 holds

ex g1, g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

let f1, f2 be S-Sequence_in_R2; :: thesis: ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 implies ex g1, g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) ) )

assume that

A1: p1 = f1 /. 1 and

A2: p1 = f2 /. 1 and

A3: p2 = f1 /. (len f1) and

A4: p2 = f2 /. (len f2) and

A5: (L~ f1) /\ (L~ f2) = {p1,p2} and

A6: P = (L~ f1) \/ (L~ f2) and

A7: q <> p1 and

A8: q in rng f1 ; :: thesis: ex g1, g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

set f19 = Rev (f1 :- q);

A9: 1 <= q .. f1 by A8, FINSEQ_4:21;

A13: 1 in dom g1 by FINSEQ_5:6;

1 in dom f2 by FINSEQ_5:6;

then 1 <= len f2 by FINSEQ_3:25;

then reconsider l = (len f2) - 1 as Element of NAT by INT_1:5;

set f29 = f2 | l;

A14: l + 1 = len f2 ;

rng (Rev (f1 :- q)) = rng (f1 :- q) by FINSEQ_5:57;

then A15: rng (Rev (f1 :- q)) c= rng f1 by A8, FINSEQ_5:55;

len f2 >= 2 by TOPREAL1:def 8;

then A16: rng f2 c= L~ f2 by Th18;

len f1 >= 2 by TOPREAL1:def 8;

then rng f1 c= L~ f1 by Th18;

then A17: (rng f2) /\ (rng f1) c= (L~ f1) /\ (L~ f2) by A16, XBOOLE_1:27;

set g2 = (f2 | l) ^ (Rev (f1 :- q));

A18: dom (f2 | l) = Seg (len (f2 | l)) by FINSEQ_1:def 3;

len (f1 :- q) >= 1 by NAT_1:14;

then A19: len (Rev (f1 :- q)) >= 1 by FINSEQ_5:def 3;

then A20: ( len (Rev (f1 :- q)) in dom (Rev (f1 :- q)) & 1 in dom (Rev (f1 :- q)) ) by FINSEQ_3:25;

A21: l < len f2 by XREAL_1:44;

then A22: len (f2 | l) = l by FINSEQ_1:59;

len f2 >= 2 by TOPREAL1:def 8;

then A23: (len f2) - 1 >= (1 + 1) - 1 by XREAL_1:9;

then A24: l in dom (f2 | l) by A22, FINSEQ_3:25;

then A25: (f2 | l) /. (len (f2 | l)) = f2 /. l by A22, FINSEQ_4:70;

A26: (Rev (f1 :- q)) /. 1 = (f1 :- q) /. (len (f1 :- q)) by FINSEQ_5:65

.= f2 /. (len f2) by A3, A4, A8, FINSEQ_5:54 ;

then A27: LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) = LSeg (f2,l) by A23, A14, A25, TOPREAL1:def 3;

then A80: not f2 | l is empty ;

f1 :- q is unfolded by A8, Th27;

then A81: Rev (f1 :- q) is unfolded by Th28;

then A96: rng g1 c= L~ g1 by Th18;

set Z = (rng (f2 | l)) /\ (rng (Rev (f1 :- q)));

A97: 1 in dom (f2 | l) by A22, A23, FINSEQ_3:25;

A98: len f2 in dom f2 by FINSEQ_5:6;

then A99: p2 .. f2 = len f2 by A4, FINSEQ_5:41;

then A102: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p1,p2} by TARSKI:def 2;

dom f2 = Seg (len f2) by FINSEQ_1:def 3;

then A103: len (f2 | l) in dom f2 by A22, A14, A24, A18, FINSEQ_2:8;

L~ (f1 :- q) c= L~ f1 by A8, Lm15;

then A113: L~ (Rev (f1 :- q)) c= L~ f1 by Th22;

L~ (f2 | l) c= L~ f2 by Lm1;

then (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) c= {p1,p2} by A5, A113, XBOOLE_1:27;

then A114: ( (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p1} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p2} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p1,p2} ) by ZFMISC_1:36;

f1 :- q is special by A8, Th39;

then A115: Rev (f1 :- q) is special by Th40;

A116: 1 in dom (f1 :- q) by FINSEQ_5:6;

then not p1 in (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) by XBOOLE_0:def 4;

then A123: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p1} by TARSKI:def 1;

rng (f2 | l) c= rng f2 by FINSEQ_5:19;

then (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) c= (rng f2) /\ (rng f1) by A15, XBOOLE_1:27;

then A124: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) c= {p1,p2} by A5, A17;

reconsider f1q = f1 :- q as one-to-one FinSequence of (TOP-REAL 2) by A8, FINSEQ_5:56;

A125: Rev f1q is one-to-one ;

f1 :- q is s.n.c. by A8, Th34;

then A126: Rev (f1 :- q) is s.n.c. by Th35;

( ((f2 | l) /. (len (f2 | l))) `1 = ((Rev (f1 :- q)) /. 1) `1 or ((f2 | l) /. (len (f2 | l))) `2 = ((Rev (f1 :- q)) /. 1) `2 ) by A23, A14, A25, A26, TOPREAL1:def 5;

then A127: (f2 | l) ^ (Rev (f1 :- q)) is special by A115, Lm13;

(len (f2 | l)) + (len (Rev (f1 :- q))) >= 1 + 1 by A22, A19, A23, XREAL_1:7;

then A128: len ((f2 | l) ^ (Rev (f1 :- q))) >= 2 by FINSEQ_1:22;

(rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p2} by A101, TARSKI:def 1;

then (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) = {} by A123, A102, A124, ZFMISC_1:36;

then rng (f2 | l) misses rng (Rev (f1 :- q)) ;

then A129: (f2 | l) ^ (Rev (f1 :- q)) is one-to-one by A125, FINSEQ_3:91;

not p1 in (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) by A32, XBOOLE_0:def 4;

then L~ (f2 | l) misses L~ (Rev (f1 :- q)) by A114, A112, TARSKI:def 1, TARSKI:def 2;

then (f2 | l) ^ (Rev (f1 :- q)) is s.n.c. by A126, A28, A47, Th36;

then reconsider g2 = (f2 | l) ^ (Rev (f1 :- q)) as S-Sequence_in_R2 by A129, A128, A82, A127, TOPREAL1:def 8;

A130: (L~ f2) \/ (L~ (Rev (f1 :- q))) = (L~ ((f2 | l) ^ <*p2*>)) \/ (L~ (Rev (f1 :- q))) by A4, A14, FINSEQ_5:21

.= ((L~ (f2 | l)) \/ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)))) \/ (L~ (Rev (f1 :- q))) by A4, A97, A26, Th19, RELAT_1:38

.= L~ g2 by A20, A80, Th23, RELAT_1:38 ;

take g1 ; :: thesis: ex g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

take g2 ; :: thesis: ( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

thus A131: p1 = g1 /. 1 by A1, A8, FINSEQ_5:44; :: thesis: ( p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

A132: 1 in dom g2 by FINSEQ_5:6;

hence A133: g2 /. 1 = g2 . 1 by PARTFUN1:def 6

.= (f2 | l) . 1 by A97, FINSEQ_1:def 7

.= (f2 | l) /. 1 by A97, PARTFUN1:def 6

.= p1 by A2, A97, FINSEQ_4:70 ;

:: thesis: ( q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

thus A134: q = g1 /. (q .. f1) by A8, FINSEQ_5:45

.= g1 /. (len g1) by A8, FINSEQ_5:42 ; :: thesis: ( q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

A135: len g2 in dom g2 by FINSEQ_5:6;

hence A136: g2 /. (len g2) = g2 . (len g2) by PARTFUN1:def 6

.= g2 . ((len (f2 | l)) + (len (Rev (f1 :- q)))) by FINSEQ_1:22

.= (Rev (f1 :- q)) . (len (Rev (f1 :- q))) by A20, FINSEQ_1:def 7

.= (Rev (f1 :- q)) . (len (f1 :- q)) by FINSEQ_5:def 3

.= (f1 :- q) . 1 by FINSEQ_5:62

.= (f1 :- q) /. 1 by A116, PARTFUN1:def 6

.= q by FINSEQ_5:53 ;

:: thesis: ( (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

len g2 >= 2 by TOPREAL1:def 8;

then A137: rng g2 c= L~ g2 by Th18;

A138: len g1 in dom g1 by FINSEQ_5:6;

thus {p1,q} = (L~ g1) /\ (L~ g2) :: thesis: P = (L~ g1) \/ (L~ g2)

.= (L~ g1) \/ ((L~ f2) \/ (L~ (f1 :- q))) by XBOOLE_1:4

.= (L~ g1) \/ (L~ g2) by A130, Th22 ; :: thesis: verum

for f1, f2 being S-Sequence_in_R2 st p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 holds

ex g1, g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

let p1, p2, q be Point of (TOP-REAL 2); :: thesis: for f1, f2 being S-Sequence_in_R2 st p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 holds

ex g1, g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

let f1, f2 be S-Sequence_in_R2; :: thesis: ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 implies ex g1, g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) ) )

assume that

A1: p1 = f1 /. 1 and

A2: p1 = f2 /. 1 and

A3: p2 = f1 /. (len f1) and

A4: p2 = f2 /. (len f2) and

A5: (L~ f1) /\ (L~ f2) = {p1,p2} and

A6: P = (L~ f1) \/ (L~ f2) and

A7: q <> p1 and

A8: q in rng f1 ; :: thesis: ex g1, g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

set f19 = Rev (f1 :- q);

A9: 1 <= q .. f1 by A8, FINSEQ_4:21;

A10: now :: thesis: not 1 = q .. f1

then reconsider g1 = f1 -: q as S-Sequence_in_R2 by A8, Th46;assume A11:
1 = q .. f1
; :: thesis: contradiction

then A12: 1 in dom f1 by A8, FINSEQ_4:20;

f1 . 1 = q by A8, A11, FINSEQ_4:19;

hence contradiction by A1, A7, A12, PARTFUN1:def 6; :: thesis: verum

end;then A12: 1 in dom f1 by A8, FINSEQ_4:20;

f1 . 1 = q by A8, A11, FINSEQ_4:19;

hence contradiction by A1, A7, A12, PARTFUN1:def 6; :: thesis: verum

A13: 1 in dom g1 by FINSEQ_5:6;

1 in dom f2 by FINSEQ_5:6;

then 1 <= len f2 by FINSEQ_3:25;

then reconsider l = (len f2) - 1 as Element of NAT by INT_1:5;

set f29 = f2 | l;

A14: l + 1 = len f2 ;

rng (Rev (f1 :- q)) = rng (f1 :- q) by FINSEQ_5:57;

then A15: rng (Rev (f1 :- q)) c= rng f1 by A8, FINSEQ_5:55;

len f2 >= 2 by TOPREAL1:def 8;

then A16: rng f2 c= L~ f2 by Th18;

len f1 >= 2 by TOPREAL1:def 8;

then rng f1 c= L~ f1 by Th18;

then A17: (rng f2) /\ (rng f1) c= (L~ f1) /\ (L~ f2) by A16, XBOOLE_1:27;

set g2 = (f2 | l) ^ (Rev (f1 :- q));

A18: dom (f2 | l) = Seg (len (f2 | l)) by FINSEQ_1:def 3;

len (f1 :- q) >= 1 by NAT_1:14;

then A19: len (Rev (f1 :- q)) >= 1 by FINSEQ_5:def 3;

then A20: ( len (Rev (f1 :- q)) in dom (Rev (f1 :- q)) & 1 in dom (Rev (f1 :- q)) ) by FINSEQ_3:25;

A21: l < len f2 by XREAL_1:44;

then A22: len (f2 | l) = l by FINSEQ_1:59;

len f2 >= 2 by TOPREAL1:def 8;

then A23: (len f2) - 1 >= (1 + 1) - 1 by XREAL_1:9;

then A24: l in dom (f2 | l) by A22, FINSEQ_3:25;

then A25: (f2 | l) /. (len (f2 | l)) = f2 /. l by A22, FINSEQ_4:70;

A26: (Rev (f1 :- q)) /. 1 = (f1 :- q) /. (len (f1 :- q)) by FINSEQ_5:65

.= f2 /. (len f2) by A3, A4, A8, FINSEQ_5:54 ;

then A27: LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) = LSeg (f2,l) by A23, A14, A25, TOPREAL1:def 3;

A28: now :: thesis: for i being Nat st 1 <= i & i + 2 <= len (f2 | l) holds

LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))

A31:
1 in dom f1
by FINSEQ_5:6;LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))

let i be Nat; :: thesis: ( 1 <= i & i + 2 <= len (f2 | l) implies LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) )

assume that

1 <= i and

A29: i + 2 <= len (f2 | l) ; :: thesis: LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))

(i + 1) + 1 <= len (f2 | l) by A29;

then A30: i + 1 < len (f2 | l) by NAT_1:13;

then LSeg ((f2 | l),i) = LSeg (f2,i) by Th3;

hence LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by A22, A27, A30, TOPREAL1:def 7; :: thesis: verum

end;assume that

1 <= i and

A29: i + 2 <= len (f2 | l) ; :: thesis: LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))

(i + 1) + 1 <= len (f2 | l) by A29;

then A30: i + 1 < len (f2 | l) by NAT_1:13;

then LSeg ((f2 | l),i) = LSeg (f2,i) by Th3;

hence LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by A22, A27, A30, TOPREAL1:def 7; :: thesis: verum

A32: now :: thesis: not p1 in L~ (Rev (f1 :- q))

A33:
1 + 1 <= len f1
by TOPREAL1:def 8;

p1 in LSeg ((f1 /. 1),(f1 /. (1 + 1))) by A1, RLTOPSP1:68;

then A34: p1 in LSeg (f1,1) by A33, TOPREAL1:def 3;

assume p1 in L~ (Rev (f1 :- q)) ; :: thesis: contradiction

then A35: p1 in L~ (f1 :- q) by Th22;

then consider i being Nat such that

A36: 1 <= i and

i + 1 <= len (f1 :- q) and

A37: p1 in LSeg ((f1 :- q),i) by Th13;

consider j being Nat such that

A38: i = j + 1 by A36, NAT_1:6;

A39: 1 < q .. f1 by A10, A9, XXREAL_0:1;

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

A40: LSeg ((f1 :- q),i) = LSeg (f1,(j + (q .. f1))) by A8, A38, Th10;

then p1 in (LSeg (f1,1)) /\ (LSeg (f1,(j + (q .. f1)))) by A37, A34, XBOOLE_0:def 4;

then A41: LSeg (f1,1) meets LSeg (f1,(j + (q .. f1))) ;

end;p1 in LSeg ((f1 /. 1),(f1 /. (1 + 1))) by A1, RLTOPSP1:68;

then A34: p1 in LSeg (f1,1) by A33, TOPREAL1:def 3;

assume p1 in L~ (Rev (f1 :- q)) ; :: thesis: contradiction

then A35: p1 in L~ (f1 :- q) by Th22;

then consider i being Nat such that

A36: 1 <= i and

i + 1 <= len (f1 :- q) and

A37: p1 in LSeg ((f1 :- q),i) by Th13;

consider j being Nat such that

A38: i = j + 1 by A36, NAT_1:6;

A39: 1 < q .. f1 by A10, A9, XXREAL_0:1;

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

A40: LSeg ((f1 :- q),i) = LSeg (f1,(j + (q .. f1))) by A8, A38, Th10;

then p1 in (LSeg (f1,1)) /\ (LSeg (f1,(j + (q .. f1)))) by A37, A34, XBOOLE_0:def 4;

then A41: LSeg (f1,1) meets LSeg (f1,(j + (q .. f1))) ;

per cases
( j = 0 or j <> 0 )
;

end;

suppose A42:
j = 0
; :: thesis: contradiction

A43:
1 + 1 <= q .. f1
by A39, NAT_1:13;

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( q .. f1 = 2 or q .. f1 > 2 )
by A43, XXREAL_0:1;

end;

suppose A44:
q .. f1 = 2
; :: thesis: contradiction

A45:
q .. f1 <= len f1
by A8, FINSEQ_4:21;

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( len f1 = 2 or len f1 > 2 )
by A44, A45, XXREAL_0:1;

end;

suppose
len f1 = 2
; :: thesis: contradiction

then
len (f1 :- q) = ((len f1) - (len f1)) + 1
by A8, A44, FINSEQ_5:50;

hence contradiction by A35, TOPREAL1:22; :: thesis: verum

end;hence contradiction by A35, TOPREAL1:22; :: thesis: verum

suppose
len f1 > 2
; :: thesis: contradiction

then
1 + 2 <= len f1
by NAT_1:13;

then (LSeg (f1,1)) /\ (LSeg (f1,(1 + 1))) = {(f1 /. (1 + 1))} by TOPREAL1:def 6;

then p1 in {(f1 /. 2)} by A37, A34, A40, A42, A44, XBOOLE_0:def 4;

then A46: p1 = f1 /. 2 by TARSKI:def 1;

2 in dom f1 by A8, A44, FINSEQ_4:20;

hence contradiction by A1, A31, A46, PARTFUN2:10; :: thesis: verum

end;then (LSeg (f1,1)) /\ (LSeg (f1,(1 + 1))) = {(f1 /. (1 + 1))} by TOPREAL1:def 6;

then p1 in {(f1 /. 2)} by A37, A34, A40, A42, A44, XBOOLE_0:def 4;

then A46: p1 = f1 /. 2 by TARSKI:def 1;

2 in dom f1 by A8, A44, FINSEQ_4:20;

hence contradiction by A1, A31, A46, PARTFUN2:10; :: thesis: verum

suppose
j <> 0
; :: thesis: contradiction

then
1 + 1 < j + (q .. f1)
by A39, NAT_1:14, XREAL_1:8;

hence contradiction by A41, TOPREAL1:def 7; :: thesis: verum

end;hence contradiction by A41, TOPREAL1:def 7; :: thesis: verum

A47: now :: thesis: for i being Nat st 2 <= i & i + 1 <= len (Rev (f1 :- q)) holds

LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))

LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))

let i be Nat; :: thesis: ( 2 <= i & i + 1 <= len (Rev (f1 :- q)) implies LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) )

assume that

A48: 2 <= i and

A49: i + 1 <= len (Rev (f1 :- q)) ; :: thesis: LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))

reconsider m = (len (Rev (f1 :- q))) - (i + 1) as Element of NAT by A49, INT_1:5;

(m + 1) + i = len (f1 :- q) by FINSEQ_5:def 3;

then A50: LSeg ((Rev (f1 :- q)),i) = LSeg ((f1 :- q),(m + 1)) by Th2

.= LSeg (f1,(m + (q .. f1))) by A8, Th10 ;

then A51: LSeg ((Rev (f1 :- q)),i) c= L~ f1 by TOPREAL3:19;

then A69: not p1 in LSeg ((Rev (f1 :- q)),i) by A32;

LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) c= L~ f2 by A27, TOPREAL3:19;

then A70: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),i)) c= {p1,p2} by A5, A51, XBOOLE_1:27;

hence LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) ; :: thesis: verum

end;assume that

A48: 2 <= i and

A49: i + 1 <= len (Rev (f1 :- q)) ; :: thesis: LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))

reconsider m = (len (Rev (f1 :- q))) - (i + 1) as Element of NAT by A49, INT_1:5;

(m + 1) + i = len (f1 :- q) by FINSEQ_5:def 3;

then A50: LSeg ((Rev (f1 :- q)),i) = LSeg ((f1 :- q),(m + 1)) by Th2

.= LSeg (f1,(m + (q .. f1))) by A8, Th10 ;

then A51: LSeg ((Rev (f1 :- q)),i) c= L~ f1 by TOPREAL3:19;

A52: now :: thesis: not p2 in LSeg ((Rev (f1 :- q)),i)

LSeg ((Rev (f1 :- q)),i) c= L~ (Rev (f1 :- q))
by TOPREAL3:19;A53:
len f1 >= 1 + 1
by TOPREAL1:def 8;

then reconsider k = (len f1) - 1 as Element of NAT by INT_1:5, XXREAL_0:2;

A54: p2 in LSeg ((f1 /. k),(f1 /. (len f1))) by A3, RLTOPSP1:68;

A55: k + 1 = len f1 ;

then 1 <= k by A53, XREAL_1:6;

then A56: p2 in LSeg (f1,k) by A55, A54, TOPREAL1:def 3;

A57: len (Rev (f1 :- q)) = len (f1 :- q) by FINSEQ_5:def 3;

A58: (len f1) - i = (((((len f1) - (q .. f1)) + 1) - 1) + (q .. f1)) - i

.= (((len (Rev (f1 :- q))) - 1) + (q .. f1)) - i by A8, A57, FINSEQ_5:50

.= m + (q .. f1) ;

end;then reconsider k = (len f1) - 1 as Element of NAT by INT_1:5, XXREAL_0:2;

A54: p2 in LSeg ((f1 /. k),(f1 /. (len f1))) by A3, RLTOPSP1:68;

A55: k + 1 = len f1 ;

then 1 <= k by A53, XREAL_1:6;

then A56: p2 in LSeg (f1,k) by A55, A54, TOPREAL1:def 3;

A57: len (Rev (f1 :- q)) = len (f1 :- q) by FINSEQ_5:def 3;

A58: (len f1) - i = (((((len f1) - (q .. f1)) + 1) - 1) + (q .. f1)) - i

.= (((len (Rev (f1 :- q))) - 1) + (q .. f1)) - i by A8, A57, FINSEQ_5:50

.= m + (q .. f1) ;

per cases
( i = 1 + 1 or i <> 2 )
;

end;

suppose A59:
i = 1 + 1
; :: thesis: not p2 in LSeg ((Rev (f1 :- q)),i)

A60:
q .. f1 <= m + (q .. f1)
by NAT_1:11;

1 <= q .. f1 by A8, FINSEQ_4:21;

then A61: 1 <= m + (q .. f1) by A60, XXREAL_0:2;

assume A62: p2 in LSeg ((Rev (f1 :- q)),i) ; :: thesis: contradiction

A63: (m + (q .. f1)) + (1 + 1) = len f1 by A58, A59;

A64: 1 <= k by A53, XREAL_1:19;

p2 in LSeg ((f1 /. k),(f1 /. (k + 1))) by A3, RLTOPSP1:68;

then A65: p2 in LSeg (f1,k) by A64, TOPREAL1:def 3;

(m + (q .. f1)) + 1 = k by A58, A59;

then (LSeg (f1,(m + (q .. f1)))) /\ (LSeg (f1,k)) = {(f1 /. k)} by A61, A63, TOPREAL1:def 6;

then p2 in {(f1 /. k)} by A50, A65, A62, XBOOLE_0:def 4;

then A66: f1 /. (len f1) = f1 /. k by A3, TARSKI:def 1;

k <= len f1 by A55, NAT_1:11;

then A67: k in dom f1 by A64, FINSEQ_3:25;

len f1 in dom f1 by FINSEQ_5:6;

then (len f1) - k = (len f1) - (len f1) by A67, A66, PARTFUN2:10

.= 0 ;

hence contradiction ; :: thesis: verum

end;1 <= q .. f1 by A8, FINSEQ_4:21;

then A61: 1 <= m + (q .. f1) by A60, XXREAL_0:2;

assume A62: p2 in LSeg ((Rev (f1 :- q)),i) ; :: thesis: contradiction

A63: (m + (q .. f1)) + (1 + 1) = len f1 by A58, A59;

A64: 1 <= k by A53, XREAL_1:19;

p2 in LSeg ((f1 /. k),(f1 /. (k + 1))) by A3, RLTOPSP1:68;

then A65: p2 in LSeg (f1,k) by A64, TOPREAL1:def 3;

(m + (q .. f1)) + 1 = k by A58, A59;

then (LSeg (f1,(m + (q .. f1)))) /\ (LSeg (f1,k)) = {(f1 /. k)} by A61, A63, TOPREAL1:def 6;

then p2 in {(f1 /. k)} by A50, A65, A62, XBOOLE_0:def 4;

then A66: f1 /. (len f1) = f1 /. k by A3, TARSKI:def 1;

k <= len f1 by A55, NAT_1:11;

then A67: k in dom f1 by A64, FINSEQ_3:25;

len f1 in dom f1 by FINSEQ_5:6;

then (len f1) - k = (len f1) - (len f1) by A67, A66, PARTFUN2:10

.= 0 ;

hence contradiction ; :: thesis: verum

suppose
i <> 2
; :: thesis: not p2 in LSeg ((Rev (f1 :- q)),i)

then
2 < i
by A48, XXREAL_0:1;

then 2 + 1 <= i by NAT_1:13;

then (len f1) - i <= (len f1) - (1 + 2) by XREAL_1:10;

then (len f1) - i <= ((len f1) - 1) - 2 ;

then A68: ((len f1) - i) + (1 + 1) <= k by XREAL_1:19;

((len f1) - i) + (1 + 1) = ((m + (q .. f1)) + 1) + 1 by A58;

then (m + (q .. f1)) + 1 < k by A68, NAT_1:13;

then LSeg (f1,k) misses LSeg (f1,(m + (q .. f1))) by TOPREAL1:def 7;

then (LSeg (f1,k)) /\ (LSeg (f1,(m + (q .. f1)))) = {} ;

hence not p2 in LSeg ((Rev (f1 :- q)),i) by A50, A56, XBOOLE_0:def 4; :: thesis: verum

end;then 2 + 1 <= i by NAT_1:13;

then (len f1) - i <= (len f1) - (1 + 2) by XREAL_1:10;

then (len f1) - i <= ((len f1) - 1) - 2 ;

then A68: ((len f1) - i) + (1 + 1) <= k by XREAL_1:19;

((len f1) - i) + (1 + 1) = ((m + (q .. f1)) + 1) + 1 by A58;

then (m + (q .. f1)) + 1 < k by A68, NAT_1:13;

then LSeg (f1,k) misses LSeg (f1,(m + (q .. f1))) by TOPREAL1:def 7;

then (LSeg (f1,k)) /\ (LSeg (f1,(m + (q .. f1)))) = {} ;

hence not p2 in LSeg ((Rev (f1 :- q)),i) by A50, A56, XBOOLE_0:def 4; :: thesis: verum

then A69: not p1 in LSeg ((Rev (f1 :- q)),i) by A32;

LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) c= L~ f2 by A27, TOPREAL3:19;

then A70: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),i)) c= {p1,p2} by A5, A51, XBOOLE_1:27;

now :: thesis: for x being object holds not x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),i))

then
(LSeg ((Rev (f1 :- q)),i)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {}
by XBOOLE_0:def 1;given x being object such that A71:
x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),i))
; :: thesis: contradiction

( x = p1 or x = p2 ) by A70, A71, TARSKI:def 2;

hence contradiction by A69, A52, A71, XBOOLE_0:def 4; :: thesis: verum

end;( x = p1 or x = p2 ) by A70, A71, TARSKI:def 2;

hence contradiction by A69, A52, A71, XBOOLE_0:def 4; :: thesis: verum

hence LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) ; :: thesis: verum

A72: now :: thesis: ( len (Rev (f1 :- q)) <> 1 implies (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) = {((Rev (f1 :- q)) /. 1)} )

A79:
len (f2 | l) >= 1
by A21, A23, FINSEQ_1:59;assume
len (Rev (f1 :- q)) <> 1
; :: thesis: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) = {((Rev (f1 :- q)) /. 1)}

then 1 < len (Rev (f1 :- q)) by A19, XXREAL_0:1;

then A73: 1 + 1 <= len (Rev (f1 :- q)) by NAT_1:13;

end;then 1 < len (Rev (f1 :- q)) by A19, XXREAL_0:1;

then A73: 1 + 1 <= len (Rev (f1 :- q)) by NAT_1:13;

now :: thesis: for x being object holds

( ( x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) implies x = (Rev (f1 :- q)) /. 1 ) & ( x = (Rev (f1 :- q)) /. 1 implies x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ) )

hence
(LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) = {((Rev (f1 :- q)) /. 1)}
by TARSKI:def 1; :: thesis: verum( ( x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) implies x = (Rev (f1 :- q)) /. 1 ) & ( x = (Rev (f1 :- q)) /. 1 implies x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ) )

let x be object ; :: thesis: ( ( x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) implies x = (Rev (f1 :- q)) /. 1 ) & ( x = (Rev (f1 :- q)) /. 1 implies x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ) )

then x in LSeg (((Rev (f1 :- q)) /. 1),((Rev (f1 :- q)) /. (1 + 1))) by RLTOPSP1:68;

then A78: x in LSeg ((Rev (f1 :- q)),1) by A73, TOPREAL1:def 3;

x in LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by A77, RLTOPSP1:68;

hence x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) by A78, XBOOLE_0:def 4; :: thesis: verum

end;hereby :: thesis: ( x = (Rev (f1 :- q)) /. 1 implies x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) )

assume A77:
x = (Rev (f1 :- q)) /. 1
; :: thesis: x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1))reconsider m = (len (Rev (f1 :- q))) - 2 as Element of NAT by A73, INT_1:5;

LSeg ((Rev (f1 :- q)),1) c= L~ (Rev (f1 :- q)) by TOPREAL3:19;

then not p1 in LSeg ((Rev (f1 :- q)),1) by A32;

then A74: not p1 in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) by XBOOLE_0:def 4;

(m + 1) + 1 = len (f1 :- q) by FINSEQ_5:def 3;

then LSeg ((Rev (f1 :- q)),1) = LSeg ((f1 :- q),(m + 1)) by Th2

.= LSeg (f1,(m + (q .. f1))) by A8, Th10 ;

then A75: LSeg ((Rev (f1 :- q)),1) c= L~ f1 by TOPREAL3:19;

LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) c= L~ f2 by A27, TOPREAL3:19;

then A76: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) c= {p1,p2} by A5, A75, XBOOLE_1:27;

assume x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ; :: thesis: x = (Rev (f1 :- q)) /. 1

hence x = (Rev (f1 :- q)) /. 1 by A4, A26, A76, A74, TARSKI:def 2; :: thesis: verum

end;LSeg ((Rev (f1 :- q)),1) c= L~ (Rev (f1 :- q)) by TOPREAL3:19;

then not p1 in LSeg ((Rev (f1 :- q)),1) by A32;

then A74: not p1 in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) by XBOOLE_0:def 4;

(m + 1) + 1 = len (f1 :- q) by FINSEQ_5:def 3;

then LSeg ((Rev (f1 :- q)),1) = LSeg ((f1 :- q),(m + 1)) by Th2

.= LSeg (f1,(m + (q .. f1))) by A8, Th10 ;

then A75: LSeg ((Rev (f1 :- q)),1) c= L~ f1 by TOPREAL3:19;

LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) c= L~ f2 by A27, TOPREAL3:19;

then A76: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) c= {p1,p2} by A5, A75, XBOOLE_1:27;

assume x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ; :: thesis: x = (Rev (f1 :- q)) /. 1

hence x = (Rev (f1 :- q)) /. 1 by A4, A26, A76, A74, TARSKI:def 2; :: thesis: verum

then x in LSeg (((Rev (f1 :- q)) /. 1),((Rev (f1 :- q)) /. (1 + 1))) by RLTOPSP1:68;

then A78: x in LSeg ((Rev (f1 :- q)),1) by A73, TOPREAL1:def 3;

x in LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by A77, RLTOPSP1:68;

hence x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) by A78, XBOOLE_0:def 4; :: thesis: verum

then A80: not f2 | l is empty ;

f1 :- q is unfolded by A8, Th27;

then A81: Rev (f1 :- q) is unfolded by Th28;

A82: now :: thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded end;

len g1 >= 2
by TOPREAL1:def 8;per cases
( ( len (f2 | l) = 1 & len (Rev (f1 :- q)) = 1 ) or ( len (f2 | l) <> 1 & len (Rev (f1 :- q)) = 1 ) or ( len (f2 | l) = 1 & len (Rev (f1 :- q)) <> 1 ) or ( len (f2 | l) <> 1 & len (Rev (f1 :- q)) <> 1 ) )
;

end;

suppose
( len (f2 | l) = 1 & len (Rev (f1 :- q)) = 1 )
; :: thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded

then
len ((f2 | l) ^ (Rev (f1 :- q))) = 1 + 1
by FINSEQ_1:22;

hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by Th26; :: thesis: verum

end;hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by Th26; :: thesis: verum

suppose that A83:
len (f2 | l) <> 1
and

A84: len (Rev (f1 :- q)) = 1 ; :: thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded

A84: len (Rev (f1 :- q)) = 1 ; :: thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded

consider k being Nat such that

A85: k + 1 = len (f2 | l) by A79, NAT_1:6;

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

A86: LSeg ((f2 | l),k) = LSeg (f2,k) by A85, Th3;

len (f2 | l) > 1 by A22, A23, A83, XXREAL_0:1;

then A87: 1 <= k by A85, NAT_1:13;

A88: Rev (f1 :- q) = <*((Rev (f1 :- q)) . 1)*> by A84, FINSEQ_5:14

.= <*((Rev (f1 :- q)) /. 1)*> by PARTFUN1:def 6, A20 ;

k + (1 + 1) <= len f2 by A22, A85;

then (LSeg ((f2 | l),k)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {((f2 | l) /. (len (f2 | l)))} by A22, A25, A27, A85, A87, A86, TOPREAL1:def 6;

hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A85, A88, Th30; :: thesis: verum

end;A85: k + 1 = len (f2 | l) by A79, NAT_1:6;

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

A86: LSeg ((f2 | l),k) = LSeg (f2,k) by A85, Th3;

len (f2 | l) > 1 by A22, A23, A83, XXREAL_0:1;

then A87: 1 <= k by A85, NAT_1:13;

A88: Rev (f1 :- q) = <*((Rev (f1 :- q)) . 1)*> by A84, FINSEQ_5:14

.= <*((Rev (f1 :- q)) /. 1)*> by PARTFUN1:def 6, A20 ;

k + (1 + 1) <= len f2 by A22, A85;

then (LSeg ((f2 | l),k)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {((f2 | l) /. (len (f2 | l)))} by A22, A25, A27, A85, A87, A86, TOPREAL1:def 6;

hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A85, A88, Th30; :: thesis: verum

suppose that A89:
len (f2 | l) = 1
and

A90: len (Rev (f1 :- q)) <> 1 ; :: thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded

A90: len (Rev (f1 :- q)) <> 1 ; :: thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded

S:
len (f2 | l) in dom (f2 | l)
by FINSEQ_3:25, A89;

f2 | l = <*((f2 | l) . (len (f2 | l)))*> by A89, FINSEQ_5:14

.= <*((f2 | l) /. (len (f2 | l)))*> by PARTFUN1:def 6, S ;

hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A90, Th29; :: thesis: verum

end;f2 | l = <*((f2 | l) . (len (f2 | l)))*> by A89, FINSEQ_5:14

.= <*((f2 | l) /. (len (f2 | l)))*> by PARTFUN1:def 6, S ;

hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A90, Th29; :: thesis: verum

suppose that A91:
len (f2 | l) <> 1
and

A92: len (Rev (f1 :- q)) <> 1 ; :: thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded

A92: len (Rev (f1 :- q)) <> 1 ; :: thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded

consider k being Nat such that

A93: k + 1 = len (f2 | l) by A79, NAT_1:6;

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

A94: k + (1 + 1) <= len f2 by A22, A93;

A95: LSeg ((f2 | l),k) = LSeg (f2,k) by A93, Th3;

len (f2 | l) > 1 by A22, A23, A91, XXREAL_0:1;

then 1 <= k by A93, NAT_1:13;

then (LSeg ((f2 | l),k)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {((f2 | l) /. (len (f2 | l)))} by A22, A25, A27, A93, A94, A95, TOPREAL1:def 6;

hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A92, A93, Th31; :: thesis: verum

end;A93: k + 1 = len (f2 | l) by A79, NAT_1:6;

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

A94: k + (1 + 1) <= len f2 by A22, A93;

A95: LSeg ((f2 | l),k) = LSeg (f2,k) by A93, Th3;

len (f2 | l) > 1 by A22, A23, A91, XXREAL_0:1;

then 1 <= k by A93, NAT_1:13;

then (LSeg ((f2 | l),k)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {((f2 | l) /. (len (f2 | l)))} by A22, A25, A27, A93, A94, A95, TOPREAL1:def 6;

hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A92, A93, Th31; :: thesis: verum

then A96: rng g1 c= L~ g1 by Th18;

set Z = (rng (f2 | l)) /\ (rng (Rev (f1 :- q)));

A97: 1 in dom (f2 | l) by A22, A23, FINSEQ_3:25;

A98: len f2 in dom f2 by FINSEQ_5:6;

then A99: p2 .. f2 = len f2 by A4, FINSEQ_5:41;

now :: thesis: not p2 in rng (f2 | l)

then A101:
not p2 in (rng (f2 | l)) /\ (rng (Rev (f1 :- q)))
by XBOOLE_0:def 4;assume A100:
p2 in rng (f2 | l)
; :: thesis: contradiction

then p2 .. (f2 | l) = p2 .. f2 by FINSEQ_5:40;

hence contradiction by A22, A99, A100, FINSEQ_4:21, XREAL_1:44; :: thesis: verum

end;then p2 .. (f2 | l) = p2 .. f2 by FINSEQ_5:40;

hence contradiction by A22, A99, A100, FINSEQ_4:21, XREAL_1:44; :: thesis: verum

then A102: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p1,p2} by TARSKI:def 2;

dom f2 = Seg (len f2) by FINSEQ_1:def 3;

then A103: len (f2 | l) in dom f2 by A22, A14, A24, A18, FINSEQ_2:8;

now :: thesis: not p2 in L~ (f2 | l)

then A112:
not p2 in (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q)))
by XBOOLE_0:def 4;
p2 in LSeg ((f2 /. (len (f2 | l))),p2)
by RLTOPSP1:68;

then A104: p2 in LSeg (f2,(len (f2 | l))) by A4, A22, A23, A14, TOPREAL1:def 3;

assume p2 in L~ (f2 | l) ; :: thesis: contradiction

then consider i being Nat such that

A105: 1 <= i and

A106: i + 1 <= len (f2 | l) and

A107: p2 in LSeg ((f2 | l),i) by Th13;

LSeg ((f2 | l),i) = LSeg (f2,i) by A106, Th3;

then A108: p2 in (LSeg (f2,i)) /\ (LSeg (f2,(len (f2 | l)))) by A107, A104, XBOOLE_0:def 4;

then A109: LSeg (f2,i) meets LSeg (f2,(len (f2 | l))) ;

A110: len f2 <> len (f2 | l) by A21, FINSEQ_1:59;

end;then A104: p2 in LSeg (f2,(len (f2 | l))) by A4, A22, A23, A14, TOPREAL1:def 3;

assume p2 in L~ (f2 | l) ; :: thesis: contradiction

then consider i being Nat such that

A105: 1 <= i and

A106: i + 1 <= len (f2 | l) and

A107: p2 in LSeg ((f2 | l),i) by Th13;

LSeg ((f2 | l),i) = LSeg (f2,i) by A106, Th3;

then A108: p2 in (LSeg (f2,i)) /\ (LSeg (f2,(len (f2 | l)))) by A107, A104, XBOOLE_0:def 4;

then A109: LSeg (f2,i) meets LSeg (f2,(len (f2 | l))) ;

A110: len f2 <> len (f2 | l) by A21, FINSEQ_1:59;

per cases
( i + 1 = len (f2 | l) or i + 1 <> len (f2 | l) )
;

end;

suppose A111:
i + 1 = len (f2 | l)
; :: thesis: contradiction

then
i + (1 + 1) = len f2
by A22;

then (LSeg (f2,i)) /\ (LSeg (f2,(len (f2 | l)))) = {(f2 /. (len (f2 | l)))} by A105, A111, TOPREAL1:def 6;

then p2 = f2 /. (len (f2 | l)) by A108, TARSKI:def 1;

hence contradiction by A4, A98, A103, A110, PARTFUN2:10; :: thesis: verum

end;then (LSeg (f2,i)) /\ (LSeg (f2,(len (f2 | l)))) = {(f2 /. (len (f2 | l)))} by A105, A111, TOPREAL1:def 6;

then p2 = f2 /. (len (f2 | l)) by A108, TARSKI:def 1;

hence contradiction by A4, A98, A103, A110, PARTFUN2:10; :: thesis: verum

suppose
i + 1 <> len (f2 | l)
; :: thesis: contradiction

then
i + 1 < len (f2 | l)
by A106, XXREAL_0:1;

hence contradiction by A109, TOPREAL1:def 7; :: thesis: verum

end;hence contradiction by A109, TOPREAL1:def 7; :: thesis: verum

L~ (f1 :- q) c= L~ f1 by A8, Lm15;

then A113: L~ (Rev (f1 :- q)) c= L~ f1 by Th22;

L~ (f2 | l) c= L~ f2 by Lm1;

then (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) c= {p1,p2} by A5, A113, XBOOLE_1:27;

then A114: ( (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p1} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p2} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p1,p2} ) by ZFMISC_1:36;

f1 :- q is special by A8, Th39;

then A115: Rev (f1 :- q) is special by Th40;

A116: 1 in dom (f1 :- q) by FINSEQ_5:6;

now :: thesis: not p1 in rng (f1 :- q)

then
not p1 in rng (Rev (f1 :- q))
by FINSEQ_5:57;set l = p1 .. (f1 :- q);

assume A117: p1 in rng (f1 :- q) ; :: thesis: contradiction

then A118: (f1 :- q) . (p1 .. (f1 :- q)) = p1 by FINSEQ_4:19;

p1 .. (f1 :- q) <> 0 by A117, FINSEQ_4:21;

then consider j being Nat such that

A119: p1 .. (f1 :- q) = j + 1 by NAT_1:6;

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

A120: p1 .. (f1 :- q) in dom (f1 :- q) by A117, FINSEQ_4:20;

then A121: j + (q .. f1) in dom f1 by A8, A119, FINSEQ_5:51;

(f1 :- q) /. (p1 .. (f1 :- q)) = f1 /. (j + (q .. f1)) by A8, A120, A119, FINSEQ_5:52;

then j + (q .. f1) = 1 by A1, A31, A120, A118, A121, PARTFUN1:def 6, PARTFUN2:10;

then A122: q .. f1 <= 1 by NAT_1:11;

1 <= q .. f1 by A8, FINSEQ_4:21;

hence contradiction by A10, A122, XXREAL_0:1; :: thesis: verum

end;assume A117: p1 in rng (f1 :- q) ; :: thesis: contradiction

then A118: (f1 :- q) . (p1 .. (f1 :- q)) = p1 by FINSEQ_4:19;

p1 .. (f1 :- q) <> 0 by A117, FINSEQ_4:21;

then consider j being Nat such that

A119: p1 .. (f1 :- q) = j + 1 by NAT_1:6;

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

A120: p1 .. (f1 :- q) in dom (f1 :- q) by A117, FINSEQ_4:20;

then A121: j + (q .. f1) in dom f1 by A8, A119, FINSEQ_5:51;

(f1 :- q) /. (p1 .. (f1 :- q)) = f1 /. (j + (q .. f1)) by A8, A120, A119, FINSEQ_5:52;

then j + (q .. f1) = 1 by A1, A31, A120, A118, A121, PARTFUN1:def 6, PARTFUN2:10;

then A122: q .. f1 <= 1 by NAT_1:11;

1 <= q .. f1 by A8, FINSEQ_4:21;

hence contradiction by A10, A122, XXREAL_0:1; :: thesis: verum

then not p1 in (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) by XBOOLE_0:def 4;

then A123: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p1} by TARSKI:def 1;

rng (f2 | l) c= rng f2 by FINSEQ_5:19;

then (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) c= (rng f2) /\ (rng f1) by A15, XBOOLE_1:27;

then A124: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) c= {p1,p2} by A5, A17;

reconsider f1q = f1 :- q as one-to-one FinSequence of (TOP-REAL 2) by A8, FINSEQ_5:56;

A125: Rev f1q is one-to-one ;

f1 :- q is s.n.c. by A8, Th34;

then A126: Rev (f1 :- q) is s.n.c. by Th35;

( ((f2 | l) /. (len (f2 | l))) `1 = ((Rev (f1 :- q)) /. 1) `1 or ((f2 | l) /. (len (f2 | l))) `2 = ((Rev (f1 :- q)) /. 1) `2 ) by A23, A14, A25, A26, TOPREAL1:def 5;

then A127: (f2 | l) ^ (Rev (f1 :- q)) is special by A115, Lm13;

(len (f2 | l)) + (len (Rev (f1 :- q))) >= 1 + 1 by A22, A19, A23, XREAL_1:7;

then A128: len ((f2 | l) ^ (Rev (f1 :- q))) >= 2 by FINSEQ_1:22;

(rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p2} by A101, TARSKI:def 1;

then (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) = {} by A123, A102, A124, ZFMISC_1:36;

then rng (f2 | l) misses rng (Rev (f1 :- q)) ;

then A129: (f2 | l) ^ (Rev (f1 :- q)) is one-to-one by A125, FINSEQ_3:91;

not p1 in (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) by A32, XBOOLE_0:def 4;

then L~ (f2 | l) misses L~ (Rev (f1 :- q)) by A114, A112, TARSKI:def 1, TARSKI:def 2;

then (f2 | l) ^ (Rev (f1 :- q)) is s.n.c. by A126, A28, A47, Th36;

then reconsider g2 = (f2 | l) ^ (Rev (f1 :- q)) as S-Sequence_in_R2 by A129, A128, A82, A127, TOPREAL1:def 8;

A130: (L~ f2) \/ (L~ (Rev (f1 :- q))) = (L~ ((f2 | l) ^ <*p2*>)) \/ (L~ (Rev (f1 :- q))) by A4, A14, FINSEQ_5:21

.= ((L~ (f2 | l)) \/ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)))) \/ (L~ (Rev (f1 :- q))) by A4, A97, A26, Th19, RELAT_1:38

.= L~ g2 by A20, A80, Th23, RELAT_1:38 ;

take g1 ; :: thesis: ex g2 being S-Sequence_in_R2 st

( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

take g2 ; :: thesis: ( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

thus A131: p1 = g1 /. 1 by A1, A8, FINSEQ_5:44; :: thesis: ( p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

A132: 1 in dom g2 by FINSEQ_5:6;

hence A133: g2 /. 1 = g2 . 1 by PARTFUN1:def 6

.= (f2 | l) . 1 by A97, FINSEQ_1:def 7

.= (f2 | l) /. 1 by A97, PARTFUN1:def 6

.= p1 by A2, A97, FINSEQ_4:70 ;

:: thesis: ( q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

thus A134: q = g1 /. (q .. f1) by A8, FINSEQ_5:45

.= g1 /. (len g1) by A8, FINSEQ_5:42 ; :: thesis: ( q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

A135: len g2 in dom g2 by FINSEQ_5:6;

hence A136: g2 /. (len g2) = g2 . (len g2) by PARTFUN1:def 6

.= g2 . ((len (f2 | l)) + (len (Rev (f1 :- q)))) by FINSEQ_1:22

.= (Rev (f1 :- q)) . (len (Rev (f1 :- q))) by A20, FINSEQ_1:def 7

.= (Rev (f1 :- q)) . (len (f1 :- q)) by FINSEQ_5:def 3

.= (f1 :- q) . 1 by FINSEQ_5:62

.= (f1 :- q) /. 1 by A116, PARTFUN1:def 6

.= q by FINSEQ_5:53 ;

:: thesis: ( (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )

len g2 >= 2 by TOPREAL1:def 8;

then A137: rng g2 c= L~ g2 by Th18;

A138: len g1 in dom g1 by FINSEQ_5:6;

thus {p1,q} = (L~ g1) /\ (L~ g2) :: thesis: P = (L~ g1) \/ (L~ g2)

proof

A145: (L~ g1) /\ (L~ g2) = ((L~ g1) /\ (L~ f2)) \/ ((L~ g1) /\ (L~ (Rev (f1 :- q)))) by A130, XBOOLE_1:23;

A146: q .. f1 in dom f1 by A8, FINSEQ_4:20;

A147: q = f1 . (q .. f1) by A8, FINSEQ_4:19

.= f1 /. (q .. f1) by A146, PARTFUN1:def 6 ;

A148: len g1 = q .. f1 by A8, FINSEQ_5:42;

end;

thus P =
((L~ (f1 -: q)) \/ (L~ (f1 :- q))) \/ (L~ f2)
by A6, A8, Th24
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (L~ g1) /\ (L~ g2) c= {p1,q}

A144:
len f1 in dom f1
by FINSEQ_5:6;let x be object ; :: thesis: ( x in {p1,q} implies b_{1} in (L~ g1) /\ (L~ g2) )

assume A139: x in {p1,q} ; :: thesis: b_{1} in (L~ g1) /\ (L~ g2)

end;assume A139: x in {p1,q} ; :: thesis: b

A145: (L~ g1) /\ (L~ g2) = ((L~ g1) /\ (L~ f2)) \/ ((L~ g1) /\ (L~ (Rev (f1 :- q)))) by A130, XBOOLE_1:23;

A146: q .. f1 in dom f1 by A8, FINSEQ_4:20;

A147: q = f1 . (q .. f1) by A8, FINSEQ_4:19

.= f1 /. (q .. f1) by A146, PARTFUN1:def 6 ;

A148: len g1 = q .. f1 by A8, FINSEQ_5:42;

per cases
( q <> p2 or q = p2 )
;

end;

suppose A149:
q <> p2
; :: thesis: (L~ g1) /\ (L~ g2) c= {p1,q}

(L~ g1) /\ (L~ f2) c= {p1,p2} by A5, A8, Lm14, XBOOLE_1:26;

then ( (L~ g1) /\ (L~ f2) = {} or (L~ g1) /\ (L~ f2) = {p1} or (L~ g1) /\ (L~ f2) = {p2} or (L~ g1) /\ (L~ f2) = {p1,p2} ) by ZFMISC_1:36;

then A162: (L~ g1) /\ (L~ f2) c= {p1} by A161, TARSKI:def 1, TARSKI:def 2;

(L~ g1) /\ (L~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22

.= {q} by A3, A8, A10, A147, A149, Th42 ;

then (L~ g1) /\ (L~ g2) c= {p1} \/ {q} by A145, A162, XBOOLE_1:9;

hence (L~ g1) /\ (L~ g2) c= {p1,q} by ENUMSET1:1; :: thesis: verum

end;

now :: thesis: not p2 in L~ g1

then A161:
not p2 in (L~ g1) /\ (L~ f2)
by XBOOLE_0:def 4;A150:
q .. f1 <= len f1
by A8, FINSEQ_4:21;

then reconsider j = (len f1) - 1 as Element of NAT by A9, INT_1:5, XXREAL_0:2;

A151: j + 1 = len f1 ;

A152: p2 in LSeg ((f1 /. j),(f1 /. (j + 1))) by A3, RLTOPSP1:68;

1 < q .. f1 by A10, A9, XXREAL_0:1;

then 1 < len f1 by A150, XXREAL_0:2;

then 1 <= j by A151, NAT_1:13;

then A153: p2 in LSeg (f1,j) by A152, TOPREAL1:def 3;

assume p2 in L~ g1 ; :: thesis: contradiction

then consider i being Nat such that

A154: 1 <= i and

A155: i + 1 <= len g1 and

A156: p2 in LSeg (g1,i) by Th13;

A157: p2 in LSeg (f1,i) by A155, A156, Th9;

q .. f1 < len f1 by A3, A147, A149, A150, XXREAL_0:1;

then A158: q .. f1 <= j by A151, NAT_1:13;

then A159: i + 1 <= j by A148, A155, XXREAL_0:2;

end;then reconsider j = (len f1) - 1 as Element of NAT by A9, INT_1:5, XXREAL_0:2;

A151: j + 1 = len f1 ;

A152: p2 in LSeg ((f1 /. j),(f1 /. (j + 1))) by A3, RLTOPSP1:68;

1 < q .. f1 by A10, A9, XXREAL_0:1;

then 1 < len f1 by A150, XXREAL_0:2;

then 1 <= j by A151, NAT_1:13;

then A153: p2 in LSeg (f1,j) by A152, TOPREAL1:def 3;

assume p2 in L~ g1 ; :: thesis: contradiction

then consider i being Nat such that

A154: 1 <= i and

A155: i + 1 <= len g1 and

A156: p2 in LSeg (g1,i) by Th13;

A157: p2 in LSeg (f1,i) by A155, A156, Th9;

q .. f1 < len f1 by A3, A147, A149, A150, XXREAL_0:1;

then A158: q .. f1 <= j by A151, NAT_1:13;

then A159: i + 1 <= j by A148, A155, XXREAL_0:2;

per cases
( i + 1 = j or i + 1 <> j )
;

end;

suppose A160:
i + 1 = j
; :: thesis: contradiction

then
i + (1 + 1) = j + 1
;

then (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} by A154, TOPREAL1:def 6;

then p2 in {(f1 /. (i + 1))} by A157, A153, A160, XBOOLE_0:def 4;

then p2 = f1 /. (i + 1) by TARSKI:def 1;

hence contradiction by A148, A147, A149, A155, A158, A160, XXREAL_0:1; :: thesis: verum

end;then (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} by A154, TOPREAL1:def 6;

then p2 in {(f1 /. (i + 1))} by A157, A153, A160, XBOOLE_0:def 4;

then p2 = f1 /. (i + 1) by TARSKI:def 1;

hence contradiction by A148, A147, A149, A155, A158, A160, XXREAL_0:1; :: thesis: verum

suppose
i + 1 <> j
; :: thesis: contradiction

then
i + 1 < j
by A159, XXREAL_0:1;

then LSeg (f1,i) misses LSeg (f1,j) by TOPREAL1:def 7;

then (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ;

hence contradiction by A157, A153, XBOOLE_0:def 4; :: thesis: verum

end;then LSeg (f1,i) misses LSeg (f1,j) by TOPREAL1:def 7;

then (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ;

hence contradiction by A157, A153, XBOOLE_0:def 4; :: thesis: verum

(L~ g1) /\ (L~ f2) c= {p1,p2} by A5, A8, Lm14, XBOOLE_1:26;

then ( (L~ g1) /\ (L~ f2) = {} or (L~ g1) /\ (L~ f2) = {p1} or (L~ g1) /\ (L~ f2) = {p2} or (L~ g1) /\ (L~ f2) = {p1,p2} ) by ZFMISC_1:36;

then A162: (L~ g1) /\ (L~ f2) c= {p1} by A161, TARSKI:def 1, TARSKI:def 2;

(L~ g1) /\ (L~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22

.= {q} by A3, A8, A10, A147, A149, Th42 ;

then (L~ g1) /\ (L~ g2) c= {p1} \/ {q} by A145, A162, XBOOLE_1:9;

hence (L~ g1) /\ (L~ g2) c= {p1,q} by ENUMSET1:1; :: thesis: verum

suppose A163:
q = p2
; :: thesis: (L~ g1) /\ (L~ g2) c= {p1,q}

p2 .. f1 = len f1
by A3, A144, FINSEQ_5:41;

then A164: len (f1 :- q) = ((len f1) - (len f1)) + 1 by A8, A163, FINSEQ_5:50

.= 0 + 1 ;

(L~ g1) /\ (L~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22

.= (L~ g1) /\ {} by A164, TOPREAL1:22

.= {} ;

hence (L~ g1) /\ (L~ g2) c= {p1,q} by A5, A8, A145, A163, Lm14, XBOOLE_1:26; :: thesis: verum

end;then A164: len (f1 :- q) = ((len f1) - (len f1)) + 1 by A8, A163, FINSEQ_5:50

.= 0 + 1 ;

(L~ g1) /\ (L~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22

.= (L~ g1) /\ {} by A164, TOPREAL1:22

.= {} ;

hence (L~ g1) /\ (L~ g2) c= {p1,q} by A5, A8, A145, A163, Lm14, XBOOLE_1:26; :: thesis: verum

.= (L~ g1) \/ ((L~ f2) \/ (L~ (f1 :- q))) by XBOOLE_1:4

.= (L~ g1) \/ (L~ g2) by A130, Th22 ; :: thesis: verum