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;
A10: now :: thesis: not 1 = q .. f1
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 reconsider g1 = f1 -: q as S-Sequence_in_R2 by A8, Th46;
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))
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;
A31: 1 in dom f1 by FINSEQ_5:6;
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))) ;
per cases ( j = 0 or j <> 0 ) ;
suppose A42: j = 0 ; :: thesis: contradiction
A43: 1 + 1 <= q .. f1 by A39, NAT_1:13;
now :: thesis: contradiction
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:21;
now :: thesis: contradiction
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:50;
hence contradiction by A35, TOPREAL1:22; :: 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 7; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
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))
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;
A52: now :: thesis: not p2 in LSeg ((Rev (f1 :- q)),i)
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) ;
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: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;
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;
end;
end;
LSeg ((Rev (f1 :- q)),i) c= L~ (Rev (f1 :- q)) 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;
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))
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;
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)) ; :: thesis: verum
end;
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)} )
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 :: 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)) ) )
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)) ) )
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: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;
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: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;
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:59;
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
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:22;
hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by Th26; :: 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 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;
suppose that A89: len (f2 | l) = 1 and
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;
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 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;
end;
end;
len g1 >= 2 by TOPREAL1:def 8;
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)
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 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:8;
now :: thesis: not p2 in L~ (f2 | l)
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;
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 6;
then p2 = f2 /. (len (f2 | l)) by A108, TARSKI:def 1;
hence contradiction by A4, A98, A103, A110, PARTFUN2:10; :: 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, 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)
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;
then not p1 in rng (Rev (f1 :- q)) by FINSEQ_5:57;
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
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (L~ g1) /\ (L~ g2) c= {p1,q}
let x be object ; :: thesis: ( x in {p1,q} implies b1 in (L~ g1) /\ (L~ g2) )
assume A139: x in {p1,q} ; :: thesis: b1 in (L~ g1) /\ (L~ g2)
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: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 ) ;
suppose A149: q <> p2 ; :: thesis: (L~ g1) /\ (L~ g2) c= {p1,q}
now :: thesis: not p2 in L~ g1
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;
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 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;
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, 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;
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;
end;
end;
thus P = ((L~ (f1 -: q)) \/ (L~ (f1 :- q))) \/ (L~ f2) by A6, A8, Th24
.= (L~ g1) \/ ((L~ f2) \/ (L~ (f1 :- q))) by XBOOLE_1:4
.= (L~ g1) \/ (L~ g2) by A130, Th22 ; :: thesis: verum