let G be _Graph; :: thesis: for W1 being Trail of G st W1 is trivial holds
ex W2 being Path of W1 st W2 is trivial
let W1 be Trail of G; :: thesis: ( W1 is trivial implies ex W2 being Path of W1 st W2 is trivial )
assume W1 is trivial ; :: thesis: not for W2 being Path of W1 holds W2 is trivial
then A1: 1 <> len W1 by Lm55;
1 <= len W1 by ABIAN:12;
then A2: 1 < len W1 by A1, XXREAL_0:1;

now :: thesis: not for P being Path of W1 holds P is trivial

per cases ( W1 is open or W1 is closed ) ;

suppose A3: W1 is open ; :: thesis: not for P being Path of W1 holds P is trivial

set P = the Path of W1;
take P = the Path of W1; :: thesis: P is trivial
A4: P .first() = W1 .first() by Th159;
A5: P .last() = W1 .last() by Th159;
W1 .first() <> W1 .last() by A3;
hence P is trivial by A4, A5, Lm55; :: thesis: verum

end;

suppose A6: W1 is closed ; :: thesis: not for W2 being Path of W1 holds W2 is trivial

defpred S₁[ Nat] means ( $1 is odd & 1 < $1 & $1 <= len W1 & W1 . $1 = W1 . (len W1) );
A7: ex k being Nat st S₁[k] by A2;
consider k being Nat such that
A8: ( S₁[k] & ( for m being Nat st S₁[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 :: thesis: ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is trivial 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 trivial and
A23: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is closed ; :: thesis: 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 :: thesis: not k2 = 1

assume k2 = 1 ; :: thesis: contradiction
then 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; :: thesis: 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; :: thesis: 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 :: thesis: 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 . k

let m be odd Element of NAT ; :: thesis: ( 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) ; :: thesis: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m <> W1 . k
consider 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; :: thesis: verum

end;

k2 + 1 <= k by A13, A29, NAT_1:13;
then A41: k2 + 1 <= len W1 by A8, XXREAL_0:2;

now :: thesis: 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() ; :: thesis: 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; :: thesis: 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 :: thesis: for z being object st z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
z in W1 .edgeSeq()

let z be object ; :: thesis: ( 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))) ; :: thesis: 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 :: thesis: 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))) ; :: thesis: 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; :: thesis: verum

end;

suppose A60: not x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ; :: thesis: z in W1 .edgeSeq()

then A61: x in dom es5 by A48, A54, XBOOLE_0:def 3;
y = es5 . x by A48, A54, A55, A60, FUNCT_4:def 1;
then z in es5 by A53, A61, FUNCT_1:1;
hence z in W1 .edgeSeq() ; :: thesis: verum

end;

end;

end;

hence z in W1 .edgeSeq() ; :: thesis: 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;
( 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;
then aaa: ( dom es5 is included_in_Seg & dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) is included_in_Seg ) by FINSEQ_1:def 13;

now :: thesis: for x, y being Nat st x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
x < y

let x, y be Nat; :: thesis: ( 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))) ; :: thesis: 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; :: thesis: verum

end;

then A69: Sgm (dom es) = (Sgm (dom es5)) ^ (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) by aaa, 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 :: thesis: ( 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 :: thesis: not (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) <> {}

assume (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) <> {} ; :: thesis: contradiction
then 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; :: thesis: 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 FINSEQ_3:39
.= card es5 by CARD_1:62
.= len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()) by A9, Th4 ;

A78: now :: thesis: not (k2 + 1) div 2 = 0

assume (k2 + 1) div 2 = 0 ; :: thesis: contradiction
then A79: 2 * ((k2 + 1) div 2) = 2 * 0 ;
2 divides k2 + 1 by PEPIN:22;
hence contradiction by A79, NAT_D:3; :: thesis: verum

end;

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;
set h = Sgm (dom es);
A83: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 15;
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) ; :: thesis: for x being Nat st 1 <= x & x <= len (W2 .edgeSeq()) holds
(W2 .edgeSeq()) . x = (Seq es) . x
let x be Nat; :: thesis: ( 1 <= x & x <= len (W2 .edgeSeq()) implies (W2 .edgeSeq()) . x = (Seq es) . x )
assume that
A85: 1 <= x and
A86: x <= len (W2 .edgeSeq()) ; :: thesis: (W2 .edgeSeq()) . x = (Seq es) . x
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 :: thesis: (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)) ; :: thesis: (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 FINSEQ_1:def 14;
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 15 ;
x in dom (es5 * (Sgm (dom es5))) by A9, A98, FINSEQ_1:def 15;
hence (Seq es) . x = W2 . (2 * x) by A97, A100, FUNCT_1:12; :: thesis: verum

end;

suppose len (Sgm (dom es5)) < x ; :: thesis: (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; :: thesis: verum

end;

end;

end;

hence (W2 .edgeSeq()) . x = (Seq es) . x by A85, A86, Def15; :: thesis: 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; :: thesis: W2 is trivial
thus W2 is trivial by A28, A17, Th130; :: thesis: verum

end;

end;

end;

hence not for W2 being Path of W1 holds W2 is trivial ; :: thesis: verum