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:31;

A10: now

assume A11: 1 = q .. f1 ; :: thesis: contradiction
then A12: 1 in dom f1 by A8, FINSEQ_4:30;
f1 . 1 = q by A8, A11, FINSEQ_4:29;
hence contradiction by A1, A7, A12, PARTFUN1:def 8; :: thesis: verum

end;

then reconsider g1 = f1 -: q as S-Sequence_in_R2 by A8, Th50;
A13: 1 in dom g1 by FINSEQ_5:6;
1 in dom f2 by FINSEQ_5:6;
then 1 <= len f2 by FINSEQ_3:27;
then reconsider l = (len f2) - 1 as Element of NAT by INT_1:18;
set f29 = f2 | l;
A14: l + 1 = len f2 ;
rng (Rev (f1 :- q)) = rng (f1 :- q) by FINSEQ_5:60;
then A15: rng (Rev (f1 :- q)) c= rng f1 by A8, FINSEQ_5:58;
len f2 >= 2 by TOPREAL1:def 10;
then A16: rng f2 c= L~ f2 by Th18;
len f1 >= 2 by TOPREAL1:def 10;
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)) by FINSEQ_3:27;
A21: l < len f2 by XREAL_1:46;
then A22: len (f2 | l) = l by FINSEQ_1:80;
len f2 >= 2 by TOPREAL1:def 10;
then A23: (len f2) - 1 >= (1 + 1) - 1 by XREAL_1:11;
then A24: l in dom (f2 | l) by A22, FINSEQ_3:27;
then A25: (f2 | l) /. (len (f2 | l)) = f2 /. l by A22, FINSEQ_4:85;
A26: (Rev (f1 :- q)) /. 1 = (f1 :- q) /. (len (f1 :- q)) by FINSEQ_5:68
.= f2 /. (len f2) by A3, A4, A8, FINSEQ_5:57 ;
then A27: LSeg ((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1) = LSeg f2,l by A23, A14, A25, TOPREAL1:def 5;

A28: now

let i be Element of 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 9; :: thesis: verum

end;

A31: 1 in dom f1 by FINSEQ_5:6;

A32: now

A33: 1 + 1 <= len f1 by TOPREAL1:def 10;
p1 in LSeg (f1 /. 1),(f1 /. (1 + 1)) by A1, RLTOPSP1:69;
then A34: p1 in LSeg f1,1 by A33, TOPREAL1:def 5;
assume p1 in L~ (Rev (f1 :- q)) ; :: thesis: contradiction
then A35: p1 in L~ (f1 :- q) by Th22;
then consider i being Element of 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 13;
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)) by XBOOLE_0:4;

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

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

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

now

per cases ( q .. f1 = 2 or q .. f1 > 2 ) by A43, XXREAL_0:1;

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

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

now

per cases ( len f1 = 2 or len f1 > 2 ) by A44, A45, XXREAL_0:1;

suppose len f1 = 2 ; :: thesis: contradiction

then len (f1 :- q) = ((len f1) - (len f1)) + 1 by A8, A44, FINSEQ_5:53;
hence contradiction by A35, TOPREAL1:28; :: thesis: verum

end;

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 8;
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:30;
hence contradiction by A1, A31, A46, PARTFUN2:17; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose q .. f1 > 2 ; :: thesis: contradiction

then 1 + 1 < j + (q .. f1) by A42;
hence contradiction by A41, TOPREAL1:def 9; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose j <> 0 ; :: thesis: contradiction

then 1 + 1 < j + (q .. f1) by A39, NAT_1:14, XREAL_1:10;
hence contradiction by A41, TOPREAL1:def 9; :: thesis: verum

end;

end;

end;

A47: now

let i be Element of 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:18;
(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:26;

A52: now

A53: len f1 >= 1 + 1 by TOPREAL1:def 10;
then reconsider k = (len f1) - 1 as Element of NAT by INT_1:18, XXREAL_0:2;
A54: p2 in LSeg (f1 /. k),(f1 /. (len f1)) by A3, RLTOPSP1:69;
A55: k + 1 = len f1 ;
then 1 <= k by A53, XREAL_1:8;
then A56: p2 in LSeg f1,k by A55, A54, TOPREAL1:def 5;
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:53
.= m + (q .. f1) ;

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

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:31;
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:21;
p2 in LSeg (f1 /. k),(f1 /. (k + 1)) by A3, RLTOPSP1:69;
then A65: p2 in LSeg f1,k by A64, TOPREAL1:def 5;
(m + (q .. f1)) + 1 = k by A58, A59;
then (LSeg f1,(m + (q .. f1))) /\ (LSeg f1,k) = {(f1 /. k)} by A61, A63, TOPREAL1:def 8;
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:27;
len f1 in dom f1 by FINSEQ_5:6;
then (len f1) - k = (len f1) - (len f1) by A67, A66, PARTFUN2:17
.= 0 ;
hence contradiction ; :: thesis: verum

end;

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:12;
then (len f1) - i <= ((len f1) - 1) - 2 ;
then A68: ((len f1) - i) + (1 + 1) <= k by XREAL_1:21;
((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 9;
then (LSeg f1,k) /\ (LSeg f1,(m + (q .. f1))) = {} by XBOOLE_0:def 7;
hence not p2 in LSeg (Rev (f1 :- q)),i by A50, A56, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

LSeg (Rev (f1 :- q)),i c= L~ (Rev (f1 :- q)) by TOPREAL3:26;
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:26;
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

given x being set 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;

then (LSeg (Rev (f1 :- q)),i) /\ (LSeg ((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) = {} by XBOOLE_0:def 1;
hence LSeg (Rev (f1 :- q)),i misses LSeg ((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1) by XBOOLE_0:def 7; :: thesis: verum

end;

A72: now

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;

now

let x be set ; :: 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) ) )

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) )

reconsider m = (len (Rev (f1 :- q))) - 2 as Element of NAT by A73, INT_1:18;
LSeg (Rev (f1 :- q)),1 c= L~ (Rev (f1 :- q)) by TOPREAL3:26;
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:26;
LSeg ((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1) c= L~ f2 by A27, TOPREAL3:26;
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;

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)
then x in LSeg ((Rev (f1 :- q)) /. 1),((Rev (f1 :- q)) /. (1 + 1)) by RLTOPSP1:69;
then A78: x in LSeg (Rev (f1 :- q)),1 by A73, TOPREAL1:def 5;
x in LSeg ((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1) by A77, RLTOPSP1:69;
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;

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

end;

A79: len (f2 | l) >= 1 by A21, A23, FINSEQ_1:80;
then A80: not f2 | l is empty ;
f1 :- q is unfolded by A8, Th28;
then A81: Rev (f1 :- q) is unfolded by Th29;

A82: now

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 ) ) ;

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:35;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by Th27; :: thesis: verum

end;

suppose that A83: len (f2 | l) <> 1 and
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 13;
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:15;
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 8;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A85, A88, Th31; :: thesis: verum

end;

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

f2 | l = <*((f2 | l) /. (len (f2 | l)))*> by A89, FINSEQ_5:15;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A90, Th30; :: thesis: verum

end;

suppose that A91: len (f2 | l) <> 1 and
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 13;
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 8;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A92, A93, Th32; :: thesis: verum

end;

end;

end;

len g1 >= 2 by TOPREAL1:def 10;
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:27;
A98: len f2 in dom f2 by FINSEQ_5:6;
then A99: p2 .. f2 = len f2 by A4, FINSEQ_5:44;

now

assume A100: p2 in rng (f2 | l) ; :: thesis: contradiction
then p2 .. (f2 | l) = p2 .. f2 by FINSEQ_5:43;
hence contradiction by A22, A99, A100, FINSEQ_4:31, XREAL_1:46; :: thesis: verum

end;

then A101: not p2 in (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) by XBOOLE_0:def 4;
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:9;

now

p2 in LSeg (f2 /. (len (f2 | l))),p2 by RLTOPSP1:69;
then A104: p2 in LSeg f2,(len (f2 | l)) by A4, A22, A23, A14, TOPREAL1:def 5;
assume p2 in L~ (f2 | l) ; :: thesis: contradiction
then consider i being Element of 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)) by XBOOLE_0:4;
A110: len f2 <> len (f2 | l) by A21, FINSEQ_1:80;

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

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 8;
then p2 = f2 /. (len (f2 | l)) by A108, TARSKI:def 1;
hence contradiction by A4, A98, A103, A110, PARTFUN2:17; :: thesis: verum

end;

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 9; :: thesis: verum

end;

end;

end;

then A112: not p2 in (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) by XBOOLE_0:def 4;
L~ (f1 :- q) c= L~ f1 by A8, Lm16;
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:42;
f1 :- q is special by A8, Th41;
then A115: Rev (f1 :- q) is special by Th42;
A116: 1 in dom (f1 :- q) by FINSEQ_5:6;

now

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:29;
p1 .. (f1 :- q) <> 0 by A117, FINSEQ_4:31;
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 13;
A120: p1 .. (f1 :- q) in dom (f1 :- q) by A117, FINSEQ_4:30;
then A121: j + (q .. f1) in dom f1 by A8, A119, FINSEQ_5:54;
(f1 :- q) /. (p1 .. (f1 :- q)) = f1 /. (j + (q .. f1)) by A8, A120, A119, FINSEQ_5:55;
then j + (q .. f1) = 1 by A1, A31, A120, A118, A121, PARTFUN1:def 8, PARTFUN2:17;
then A122: q .. f1 <= 1 by NAT_1:11;
1 <= q .. f1 by A8, FINSEQ_4:31;
hence contradiction by A10, A122, XXREAL_0:1; :: thesis: verum

end;

then not p1 in rng (Rev (f1 :- q)) by FINSEQ_5:60;
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:21;
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, XBOOLE_1:1;
reconsider f1q = f1 :- q as one-to-one FinSequence of (TOP-REAL 2) by A8, FINSEQ_5:59;
A125: Rev f1q is one-to-one ;
f1 :- q is s.n.c. by A8, Th35;
then A126: Rev (f1 :- q) is s.n.c. by Th36;
( ((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 7;
then A127: (f2 | l) ^ (Rev (f1 :- q)) is special by A115, Lm14;
(len (f2 | l)) + (len (Rev (f1 :- q))) >= 1 + 1 by A22, A19, A23, XREAL_1:9;
then A128: len ((f2 | l) ^ (Rev (f1 :- q))) >= 2 by FINSEQ_1:35;
(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:42;
then rng (f2 | l) misses rng (Rev (f1 :- q)) by XBOOLE_0:def 7;
then A129: (f2 | l) ^ (Rev (f1 :- q)) is one-to-one by A125, FINSEQ_3:98;
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, XBOOLE_0:def 7;
then (f2 | l) ^ (Rev (f1 :- q)) is s.n.c. by A126, A28, A47, Th37;
then reconsider g2 = (f2 | l) ^ (Rev (f1 :- q)) as S-Sequence_in_R2 by A129, A128, A82, A127, TOPREAL1:def 10;
A130: (L~ f2) \/ (L~ (Rev (f1 :- q))) = (L~ ((f2 | l) ^ <*p2*>)) \/ (L~ (Rev (f1 :- q))) by A4, A14, FINSEQ_5:24
.= ((L~ (f2 | l)) \/ (LSeg ((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) \/ (L~ (Rev (f1 :- q))) by A4, A97, A26, Th19, RELAT_1:60
.= L~ g2 by A20, A80, Th23, RELAT_1:60 ;
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:47; :: 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 8
.= (f2 | l) . 1 by A97, FINSEQ_1:def 7
.= (f2 | l) /. 1 by A97, PARTFUN1:def 8
.= p1 by A2, A97, FINSEQ_4:85 ;
:: 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:48
.= g1 /. (len g1) by A8, FINSEQ_5:45 ; :: 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 8
.= g2 . ((len (f2 | l)) + (len (Rev (f1 :- q)))) by FINSEQ_1:35
.= (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:65
.= (f1 :- q) /. 1 by A116, PARTFUN1:def 8
.= q by FINSEQ_5:56 ;
:: thesis: ( (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) )
len g2 >= 2 by TOPREAL1:def 10;
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

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (L~ g1) /\ (L~ g2) c= {p1,q}

let x be set ; :: thesis: ( x in {p1,q} implies b₁ in (L~ g1) /\ (L~ g2) )
assume A139: x in {p1,q} ; :: thesis: b₁ in (L~ g1) /\ (L~ g2)

per cases ( x = p1 or x = q ) by A139, TARSKI:def 2;

suppose A140: x = p1 ; :: thesis: b₁ in (L~ g1) /\ (L~ g2)

A141: p1 in rng g2 by A132, A133, PARTFUN2:4;
p1 in rng g1 by A131, A13, PARTFUN2:4;
hence x in (L~ g1) /\ (L~ g2) by A96, A137, A140, A141, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A142: x = q ; :: thesis: b₁ in (L~ g1) /\ (L~ g2)

A143: q in rng g2 by A135, A136, PARTFUN2:4;
q in rng g1 by A134, A138, PARTFUN2:4;
hence x in (L~ g1) /\ (L~ g2) by A96, A137, A142, A143, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A144: len f1 in dom f1 by FINSEQ_5:6;
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:30;
A147: q = f1 . (q .. f1) by A8, FINSEQ_4:29
.= f1 /. (q .. f1) by A146, PARTFUN1:def 8 ;
A148: len g1 = q .. f1 by A8, FINSEQ_5:45;

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

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

now

A150: q .. f1 <= len f1 by A8, FINSEQ_4:31;
then reconsider j = (len f1) - 1 as Element of NAT by A9, INT_1:18, XXREAL_0:2;
A151: j + 1 = len f1 ;
A152: p2 in LSeg (f1 /. j),(f1 /. (j + 1)) by A3, RLTOPSP1:69;
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 5;
assume p2 in L~ g1 ; :: thesis: contradiction
then consider i being Element of 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 ) ;

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 8;
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;

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 9;
then (LSeg f1,i) /\ (LSeg f1,j) = {} by XBOOLE_0:def 7;
hence contradiction by A157, A153, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

then A161: not p2 in (L~ g1) /\ (L~ f2) by XBOOLE_0:def 4;
(L~ g1) /\ (L~ f2) c= {p1,p2} by A5, A8, Lm15, 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:42;
then A162: (L~ g1) /\ (L~ f2) c= {p1} by A161, TARSKI:def 1, TARSKI:def 2, ZFMISC_1:39;
(L~ g1) /\ (L~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22
.= {q} by A3, A8, A10, A147, A149, Th45 ;
then (L~ g1) /\ (L~ g2) c= {p1} \/ {q} by A145, A162, XBOOLE_1:9;
hence (L~ g1) /\ (L~ g2) c= {p1,q} by ENUMSET1:41; :: thesis: verum

end;

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

p2 .. f1 = len f1 by A3, A144, FINSEQ_5:44;
then A164: len (f1 :- q) = ((len f1) - (len f1)) + 1 by A8, A163, FINSEQ_5:53
.= 0 + 1 ;
(L~ g1) /\ (L~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22
.= (L~ g1) /\ {} by A164, TOPREAL1:28
.= {} ;
hence (L~ g1) /\ (L~ g2) c= {p1,q} by A5, A8, A145, A163, Lm15, XBOOLE_1:26; :: thesis: verum

end;

end;

end;

thus P = ((L~ (f1 -: q)) \/ (L~ (f1 :- q))) \/ (L~ f2) by A6, A8, Th25
.= (L~ g1) \/ ((L~ f2) \/ (L~ (f1 :- q))) by XBOOLE_1:4
.= (L~ g1) \/ (L~ g2) by A130, Th22 ; :: thesis: verum