let G be _Graph; for W1 being Trail of G st W1 is V5() holds
ex W2 being Path of W1 st W2 is V5()
let W1 be Trail of G; ( W1 is V5() implies ex W2 being Path of W1 st W2 is V5() )
assume
W1 is V5()
; not for W2 being Path of W1 holds W2 is V5()
then A1:
1 <> len W1
by Lm55;
1 <= len W1
by ABIAN:12;
then A2:
1 < len W1
by A1, XXREAL_0:1;
now not for P being Path of W1 holds P is V5()per cases
( W1 is open or W1 is closed )
;
suppose A6:
W1 is
closed
;
not for W2 being Path of W1 holds W2 is V5()defpred S1[
Nat]
means ( $1 is
odd & 1
< $1 & $1
<= len W1 &
W1 . $1
= W1 . (len W1) );
A7:
ex
k being
Nat st
S1[
k]
by A2;
consider k being
Nat such that A8:
(
S1[
k] & ( for
m being
Nat st
S1[
m] holds
k <= m ) )
from NAT_1:sch 5(A7);
reconsider k =
k as
odd Element of
NAT by A8, ORDINAL1:def 12;
1
+ 1
< k + 1
by A8, XREAL_1:8;
then
2
<= k
by NAT_1:13;
then reconsider k2 =
k - (2 * 1) as
odd Element of
NAT by INT_1:5;
set W3 =
W1 .remove (
k,
(len W1));
set W4 =
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2);
set W5 = the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2);
consider es5 being
Subset of
(((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()) such that A9:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.edgeSeq() = Seq es5
by Def32;
A10:
((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq() c= (W1 .remove (k,(len W1))) .edgeSeq()
by Lm43;
W1 . k = W1 .last()
by A8;
then A11:
W1 .remove (
k,
(len W1))
= W1 .cut (1,
k)
by Th55;
then
(W1 .remove (k,(len W1))) .edgeSeq() c= W1 .edgeSeq()
by Lm43;
then
((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq() c= W1 .edgeSeq()
by A10, XBOOLE_1:1;
then reconsider es5 =
es5 as
Subset of
(W1 .edgeSeq()) by XBOOLE_1:1;
A12:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
is_Walk_from ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .first() ,
((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .last()
by Def32;
A13:
(len (W1 .remove (k,(len W1)))) + (len W1) = (len W1) + k
by A8, Lm24;
then A14:
k2 <= (len (W1 .remove (k,(len W1)))) - 0
by XREAL_1:13;
A15:
1
<= k2
by ABIAN:12;
then
((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .last() = (W1 .remove (k,(len W1))) . k2
by A14, Lm16;
then A16:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.last() = (W1 .remove (k,(len W1))) . k2
by A12;
k2 in dom (W1 .remove (k,(len W1)))
by A14, A15, FINSEQ_3:25;
then A17:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.last() = W1 . k2
by A8, A16, A11, Lm23;
((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .first() = (W1 .remove (k,(len W1))) . 1
by A14, A15, Lm16;
then A18:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.first() = (W1 .remove (k,(len W1))) . 1
by A12;
A19:
W1 . 1
= W1 . (len W1)
by A6;
A20:
now ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is V5() implies not the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is closed )
1
<= len (W1 .remove (k,(len W1)))
by ABIAN:12;
then A21:
(2 * 0) + 1
in dom (W1 .remove (k,(len W1)))
by FINSEQ_3:25;
assume that A22:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2) is
V5()
and A23:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2) is
closed
;
contradiction
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.first() = W1 . k2
by A17, A23;
then A24:
W1 . k2 = W1 . (len W1)
by A19, A8, A18, A11, A21, Lm23;
now not k2 = 1assume
k2 = 1
;
contradictionthen
len ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) = 1
by A14, Lm22;
then A25:
len the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
<= 1
by Lm72;
1
<= len the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
by ABIAN:12;
then
len the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
= 1
by A25, XXREAL_0:1;
hence
contradiction
by A22, Lm55;
verum end; then A26:
1
< k2
by A15, XXREAL_0:1;
A27:
k2 < k - 0
by XREAL_1:15;
then
k2 <= len W1
by A8, XXREAL_0:2;
hence
contradiction
by A8, A24, A26, A27;
verum end; set e =
W1 . (k2 + 1);
set W2 = the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.addEdge (W1 . (k2 + 1));
k2 < (len W1) - 0
by A8, XREAL_1:15;
then A28:
W1 . (k2 + 1) Joins W1 . k2,
W1 . (k2 + 2),
G
by Def3;
A29:
k2 < (len (W1 .remove (k,(len W1)))) - 0
by A13, XREAL_1:15;
then A30:
len ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) = k2
by Lm22;
A31:
now for m being odd Element of NAT st 1 < m & m <= len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) holds
the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m <> W1 . klet m be
odd Element of
NAT ;
( 1 < m & m <= len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) implies the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m <> W1 . k )assume that A32:
1
< m
and A33:
m <= len the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
;
the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m <> W1 . kconsider n being
odd Element of
NAT such that A34:
m <= n
and A35:
n <= len ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2))
and A36:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
. m = ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) . n
by A33, Th162;
A37:
1
< n
by A32, A34, XXREAL_0:2;
then
n in dom ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2))
by A35, FINSEQ_3:25;
then A38:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
. m = (W1 .remove (k,(len W1))) . n
by A14, A36, Lm23;
A39:
n + 0 < k2 + 2
by A30, A35, XREAL_1:8;
then A40:
n <= len W1
by A8, XXREAL_0:2;
n in dom (W1 .remove (k,(len W1)))
by A13, A37, A39, FINSEQ_3:25;
then
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
. m = W1 . n
by A8, A11, A38, Lm23;
hence
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
. m <> W1 . k
by A8, A37, A39, A40;
verum end;
k2 + 1
<= k
by A13, A29, NAT_1:13;
then A41:
k2 + 1
<= len W1
by A8, XXREAL_0:2;
now not W1 . (k2 + 1) in the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edges() assume A42:
W1 . (k2 + 1) in the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.edges()
;
contradiction
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.edges() c= ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edges()
by Th161;
then consider n being
even Element of
NAT such that A43:
1
<= n
and A44:
n <= len ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2))
and A45:
((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) . n = W1 . (k2 + 1)
by A42, Lm46;
A46:
n < k2 + 1
by A30, A44, NAT_1:13;
n <= k2 + 2
by A30, A44, NAT_1:12;
then A47:
n in dom (W1 .remove (k,(len W1)))
by A13, A43, FINSEQ_3:25;
n in dom ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2))
by A43, A44, FINSEQ_3:25;
then
W1 . (k2 + 1) = (W1 .remove (k,(len W1))) . n
by A14, A45, Lm23;
then
W1 . (k2 + 1) = W1 . n
by A8, A11, A47, Lm23;
hence
contradiction
by A41, A43, A46, Lm57;
verum end; then reconsider W2 = the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.addEdge (W1 . (k2 + 1)) as
Path of
G by A28, A17, A20, A31, Th148;
set g =
((k2 + 1) div 2) .--> (W1 . (k2 + 1));
set es =
es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)));
A48:
dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) = (dom es5) \/ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))
by FUNCT_4:def 1;
A50:
(((k2 + 1) div 2) .--> (W1 . (k2 + 1))) . ((k2 + 1) div 2) = W1 . (k2 + 1)
by FUNCOP_1:72;
A51:
now for z being object st z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
z in W1 .edgeSeq() let z be
object ;
( z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) implies z in W1 .edgeSeq() )assume A52:
z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))
;
z in W1 .edgeSeq() then consider x,
y being
object such that A53:
z = [x,y]
by RELAT_1:def 1;
A54:
x in dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))
by A52, A53, FUNCT_1:1;
A55:
y = (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) . x
by A52, A53, FUNCT_1:1;
now z in W1 .edgeSeq() per cases
( x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) or not x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) )
;
suppose A56:
x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))
;
z in W1 .edgeSeq() then A57:
x = (k2 + 1) div 2
by TARSKI:def 1;
A58:
1
<= k2 + 1
by NAT_1:12;
then
W1 . (k2 + 1) = (W1 .edgeSeq()) . x
by A41, A57, Lm40;
then A59:
(W1 .edgeSeq()) . x = y
by A48, A50, A54, A55, A56, A57, FUNCT_4:def 1;
x in dom (W1 .edgeSeq())
by A41, A57, A58, Lm40;
hence
z in W1 .edgeSeq()
by A53, A59, FUNCT_1:1;
verum end; end; end; hence
z in W1 .edgeSeq()
;
verum end; then
es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) c= W1 .edgeSeq()
by TARSKI:def 3;
then
dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) c= dom (W1 .edgeSeq())
by RELAT_1:11;
then A62:
dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) c= Seg (len (W1 .edgeSeq()))
by FINSEQ_1:def 3;
then reconsider es =
es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) as
FinSubsequence by FINSEQ_1:def 12;
reconsider es =
es as
Subset of
(W1 .edgeSeq()) by A51, TARSKI:def 3;
A63:
dom es5 c= dom (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq())
by FINSEQ_6:151;
now ( dom es5 c= Seg (len (W1 .edgeSeq())) & dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) c= Seg (len (W1 .edgeSeq())) & ( for x, y being Nat st x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
x < y ) )thus
(
dom es5 c= Seg (len (W1 .edgeSeq())) &
dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) c= Seg (len (W1 .edgeSeq())) )
by A48, A62, XBOOLE_1:11;
for x, y being Nat st x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
x < ylet x,
y be
Nat;
( x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) implies x < y )assume that A64:
x in dom es5
and A65:
y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))
;
x < y
x <= len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq())
by A63, A64, FINSEQ_3:25;
then
2
* x <= 2
* (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()))
by XREAL_1:64;
then
(2 * x) + 1
<= (2 * (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()))) + 1
by XREAL_1:7;
then A66:
(2 * x) + 1
<= k2
by A30, Def15;
A67:
2
divides k2 + 1
by PEPIN:22;
y = (k2 + 1) div 2
by A65, TARSKI:def 1;
then
2
* y = k2 + 1
by A67, NAT_D:3;
then
(2 * x) + 1
< 2
* y
by A66, NAT_1:13;
then A68:
((2 * x) + 1) - 1
< (2 * y) - 0
by XREAL_1:14;
then
x <= y
by XREAL_1:68;
hence
x < y
by A68, XXREAL_0:1;
verum end; then A69:
Sgm (dom es) = (Sgm (dom es5)) ^ (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))))
by A48, FINSEQ_3:42;
A70:
k2 in dom (W1 .remove (k,(len W1)))
by A15, A29, FINSEQ_3:25;
then A71:
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.last() = W1 . k2
by A8, A16, A11, Lm23;
now ( len (W2 .edgeSeq()) = len (Seq es) & ( for x being Nat st 1 <= x & x <= len (W2 .edgeSeq()) holds
(W2 .edgeSeq()) . x = (Seq es) . x ) )now not (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) <> {} assume
(dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) <> {}
;
contradictionthen consider x being
object such that A72:
x in (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))
by XBOOLE_0:def 1;
x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))
by A72;
then A73:
x = (k2 + 1) div 2
by TARSKI:def 1;
x in dom es5
by A72, XBOOLE_0:def 4;
then
(k2 + 1) div 2
<= len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq())
by A63, A73, FINSEQ_3:25;
then A74:
2
* ((k2 + 1) div 2) <= 2
* (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()))
by XREAL_1:64;
2
divides k2 + 1
by PEPIN:22;
then
k2 + 1
<= 2
* (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()))
by A74, NAT_D:3;
then
(k2 + 1) + 1
<= (2 * (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()))) + 1
by XREAL_1:7;
then
(1 + 1) + k2 <= 0 + k2
by A30, Def15;
hence
contradiction
by XREAL_1:6;
verum end; then A75:
dom es5 misses dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))
by XBOOLE_0:def 7;
len W2 = (len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) + 2
by A28, A71, Lm37;
then A76:
(len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) + 2
= (2 * (len (W2 .edgeSeq()))) + 1
by Def15;
A77:
len (Sgm (dom es5)) =
card (dom es5)
by A48, A62, FINSEQ_3:39, XBOOLE_1:11
.=
card es5
by CARD_1:62
.=
len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq())
by A9, Th4
;
A80:
Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) = <*((k2 + 1) div 2)*>
by A78, FINSEQ_3:44;
then A81:
len (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) = 1
by FINSEQ_1:40;
A82:
(Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) . 1
= (k2 + 1) div 2
by A80, FINSEQ_1:40;
set h =
Sgm (dom es);
A83:
Seq es = es * (Sgm (dom es))
by FINSEQ_1:def 14;
len (Seq es) =
card es
by Th4
.=
card (dom es)
by CARD_1:62
;
then len (Seq es) =
(card (dom es5)) + (card (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))))
by A48, A75, CARD_2:40
.=
(card (dom es5)) + 1
by CARD_1:30
.=
(card es5) + 1
by CARD_1:62
.=
(len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq())) + 1
by A9, Th4
;
then A84:
(2 * (len (Seq es))) + 1 =
((2 * (len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()))) + 1) + 2
.=
(2 * (len (W2 .edgeSeq()))) + 1
by A76, Def15
;
hence
len (W2 .edgeSeq()) = len (Seq es)
;
for x being Nat st 1 <= x & x <= len (W2 .edgeSeq()) holds
(W2 .edgeSeq()) . x = (Seq es) . xlet x be
Nat;
( 1 <= x & x <= len (W2 .edgeSeq()) implies (W2 .edgeSeq()) . x = (Seq es) . x )assume that A85:
1
<= x
and A86:
x <= len (W2 .edgeSeq())
;
(W2 .edgeSeq()) . x = (Seq es) . xA87:
dom es5 c= Seg (len (W1 .edgeSeq()))
by A48, A62, XBOOLE_1:11;
A88:
x in dom (Seq es)
by A84, A85, A86, FINSEQ_3:25;
then A89:
(Sgm (dom es)) . x in dom es
by A83, FUNCT_1:11;
A90:
dom (Sgm (dom es)) = Seg ((len (Sgm (dom es5))) + (len (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))))))
by A69, FINSEQ_1:def 7;
A91:
W1 . (k2 + 1) Joins the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.last() ,
W1 . k,
G
by A8, A28, A16, A11, A70, Lm23;
A92:
(Seq es) . x = es . ((Sgm (dom es)) . x)
by A83, A88, FUNCT_1:12;
A93:
x in dom (Sgm (dom es))
by A83, A88, FUNCT_1:11;
now (Seq es) . x = W2 . (2 * x)per cases
( x <= len (Sgm (dom es5)) or len (Sgm (dom es5)) < x )
;
suppose A94:
x <= len (Sgm (dom es5))
;
(Seq es) . x = W2 . (2 * x)then A95:
x in dom (Sgm (dom es5))
by A85, FINSEQ_3:25;
then A96:
(Sgm (dom es)) . x = (Sgm (dom es5)) . x
by A69, FINSEQ_1:def 7;
rng (Sgm (dom es5)) = dom es5
by A87, FINSEQ_1:def 13;
then
(Sgm (dom es)) . x in dom es5
by A95, A96, FUNCT_1:def 3;
then
not
(Sgm (dom es)) . x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))
by A75, XBOOLE_0:3;
then A97:
(Seq es) . x = es5 . ((Sgm (dom es5)) . x)
by A48, A89, A92, A96, FUNCT_4:def 1;
A98:
x in dom ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq())
by A85, A77, A94, FINSEQ_3:25;
then A99:
2
* x in dom the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
by Lm41;
( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()) . x = the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
. (2 * x)
by A85, A77, A94, Def15;
then A100:
W2 . (2 * x) =
( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()) . x
by A91, A99, Lm38
.=
(es5 * (Sgm (dom es5))) . x
by A9, FINSEQ_1:def 14
;
x in dom (es5 * (Sgm (dom es5)))
by A9, A98, FINSEQ_1:def 14;
hence
(Seq es) . x = W2 . (2 * x)
by A97, A100, FUNCT_1:12;
verum end; suppose
len (Sgm (dom es5)) < x
;
(Seq es) . x = W2 . (2 * x)then A101:
(len (Sgm (dom es5))) + 1
<= x
by NAT_1:13;
x <= (len (Sgm (dom es5))) + 1
by A93, A90, A81, FINSEQ_1:1;
then A102:
x = (len (Sgm (dom es5))) + 1
by A101, XXREAL_0:1;
1
in dom (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))))
by A81, FINSEQ_3:25;
then A103:
(Sgm (dom es)) . x = (k2 + 1) div 2
by A69, A82, A102, FINSEQ_1:def 7;
then
(Sgm (dom es)) . x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))
by TARSKI:def 1;
then A104:
(Seq es) . x =
(((k2 + 1) div 2) .--> (W1 . (k2 + 1))) . ((k2 + 1) div 2)
by A48, A89, A92, A103, FUNCT_4:def 1
.=
W1 . (k2 + 1)
by FUNCOP_1:72
.=
W2 . ((len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) + 1)
by A91, Lm38
;
2
* x =
((2 * (len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()))) + 1) + 1
by A77, A102
.=
(len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) + 1
by Def15
;
hence
(Seq es) . x = W2 . (2 * x)
by A104;
verum end; end; end; hence
(W2 .edgeSeq()) . x = (Seq es) . x
by A85, A86, Def15;
verum end; then A105:
W2 .edgeSeq() = Seq es
by FINSEQ_1:14;
1
<= len (W1 .remove (k,(len W1)))
by ABIAN:12;
then
(2 * 0) + 1
in dom (W1 .remove (k,(len W1)))
by FINSEQ_3:25;
then
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
.first() = W1 .first()
by A8, A18, A11, Lm23;
then
the
Path of
(W1 .remove (k,(len W1))) .cut (
((2 * 0) + 1),
k2)
is_Walk_from W1 .first() ,
W1 . k2
by A71;
then
W2 is_Walk_from W1 .first() ,
W1 .last()
by A8, A28, Lm39;
then reconsider W2 =
W2 as
Path of
W1 by A105, Def32;
take W2 =
W2;
W2 is V5()thus
W2 is
V5()
by A28, A17, Th130;
verum end; end; end;
hence
not for W2 being Path of W1 holds W2 is V5()
; verum