let P be Subset of (TOP-REAL 2); 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); 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; ( 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
; 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;
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 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;
( 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)
;
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;
verum end;
A31:
1 in dom f1
by FINSEQ_5:6;
A32:
now 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))
;
contradictionthen 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
;
contradictionA43:
1
+ 1
<= q .. f1
by A39, NAT_1:13;
now contradictionper cases
( q .. f1 = 2 or q .. f1 > 2 )
by A43, XXREAL_0:1;
suppose A44:
q .. f1 = 2
;
contradictionA45:
q .. f1 <= len f1
by A8, FINSEQ_4:21;
now contradictionper cases
( len f1 = 2 or len f1 > 2 )
by A44, A45, XXREAL_0:1;
suppose
len f1 > 2
;
contradictionthen
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;
verum end; end; end; hence
contradiction
;
verum end; end; end; hence
contradiction
;
verum end; end; end;
A47:
now 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;
( 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))
;
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 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
;
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)
;
contradictionA63:
(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
;
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;
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))
;
verum end;
A72:
now ( 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
;
(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 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 ;
( ( 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 ( 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))
;
x = (Rev (f1 :- q)) /. 1hence
x = (Rev (f1 :- q)) /. 1
by A4, A26, A76, A74, TARSKI:def 2;
verum
end; assume A77:
x = (Rev (f1 :- q)) /. 1
;
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;
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;
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 (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 that A83:
len (f2 | l) <> 1
and A84:
len (Rev (f1 :- q)) = 1
;
(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;
verum end; suppose that A91:
len (f2 | l) <> 1
and A92:
len (Rev (f1 :- q)) <> 1
;
(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;
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;
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 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)
;
contradictionthen 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 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 not p1 in rng (f1 :- q)set l =
p1 .. (f1 :- q);
assume A117:
p1 in rng (f1 :- q)
;
contradictionthen 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;
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
; 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
; ( 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; ( 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
;
( 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
; ( 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
;
( (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)
P = (L~ g1) \/ (L~ g2)proof
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
;
(L~ g1) /\ (L~ g2) c= {p1,q}now not p2 in L~ g1A150:
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
;
contradictionthen 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
;
contradictionthen
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;
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;
verum end; suppose A163:
q = p2
;
(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;
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
; verum