defpred S₁[ Nat] means for W1 being DWalk of G st W1 .length() = G holds
ex W2 being Path of W1 st W2 is directed ;
A1: W .length() = W .length() ;

let k be Nat; :: thesis:
assume A2: S₁[k] ; :: thesis:
let W1 be DWalk of G; :: thesis:
set WA = W1 .cut (1,((2 * k) + 1));
set e = W1 . (((2 * k) + 1) + 1);
set v = W1 . (((2 * k) + 1) + 2);
assume A3: W1 .length() = k + 1 ; :: thesis:
then A4: len W1 = (2 * (k + 1)) + 1 by Def15
.= ((2 * k) + 1) + 2 ;
then A5: (((2 * k) + 1) + 2) - 2 < (len W1) - 0 by XREAL_1:15;
then A6: W1 . (((2 * k) + 1) + 1) DJoins W1 . ((2 * k) + 1),W1 . (((2 * k) + 1) + 2),G by Lm51;
len (W1 .cut (1,((2 * k) + 1))) = (2 * k) + 1 by A5, Lm22;
then A7: (2 * k) + 1 = (2 * ((W1 .cut (1,((2 * k) + 1))) .length())) + 1 by Def15;
then consider WB being Path of W1 .cut (1,((2 * k) + 1)) such that
A8: WB is directed by A2;
A9: (W1 .cut (1,((2 * k) + 1))) .edgeSeq() c= W1 .edgeSeq() by Lm43;
A10: WB is_Walk_from (W1 .cut (1,((2 * k) + 1))) .first() ,(W1 .cut (1,((2 * k) + 1))) .last() by Def32;
A11: 1 <= (2 * k) + 1 by NAT_1:12;
then A12: (W1 .cut (1,((2 * k) + 1))) .last() = W1 . ((2 * k) + 1) by A5, Lm16, JORDAN12:2;
A13: (W1 .cut (1,((2 * k) + 1))) .first() = W1 . 1 by A5, A11, Lm16, JORDAN12:2;
then A14: WB .first() = W1 . 1 by A10;
A15: WB .last() = W1 . ((2 * k) + 1) by A10, A12;
then A16: W1 . (((2 * k) + 1) + 1) Joins WB .last() ,W1 . (((2 * k) + 1) + 2),G by A6, GLIB_000:16;

per cases ;

suppose A17: WB is closed ; :: thesis:

set W2 = W1 .remove (1,((2 * k) + 1));
W1 .first() = W1 . ((2 * k) + 1) by A14, A15, A17;
then W1 .remove (1,((2 * k) + 1)) = W1 .cut (((2 * k) + 1),(((2 * k) + 1) + 2)) by A4, Lm32;
then (len (W1 .remove (1,((2 * k) + 1)))) + ((2 * k) + 1) = (((2 * k) + 1) + 2) + 1 by A4, A5, Lm15
.= ((2 * k) + 1) + (2 + 1) ;
then reconsider W2 = W1 .remove (1,((2 * k) + 1)) as Path of W1 by Lm69;
take W2 = W2; :: thesis:
thus W2 is directed ; :: thesis:

end;

suppose A18: WB is open ; :: thesis:

consider esb being Subset of ((W1 .cut (1,((2 * k) + 1))) .edgeSeq()) such that
A19: WB .edgeSeq() = Seq esb by Def32;
A20: Seq esb is one-to-one by A19, Def27;
A21: Seq esb = esb * (Sgm (dom esb)) by FINSEQ_1:def 15;

A22: now :: thesis:

let x be object ; :: thesis:
assume x in dom esb ; :: thesis:
then [x,(esb . x)] in esb by FUNCT_1:1;
then x in dom ((W1 .cut (1,((2 * k) + 1))) .edgeSeq()) by FUNCT_1:1;
hence x in Seg k by A7, FINSEQ_1:def 3; :: thesis:

end;

then A23: dom esb c= Seg k by TARSKI:def 3;
rng (Sgm (dom esb)) = dom esb by FINSEQ_1:def 14;
then A24: Sgm (dom esb) is one-to-one by A21, A20, FUNCT_1:26;

now :: thesis:

per cases ;

suppose A25: W1 . (((2 * k) + 1) + 2) in WB .vertices() ; :: thesis:

reconsider WB9 = WB as directed Path of G by A8;
A26: dom (Sgm (dom esb)) = dom (WB .edgeSeq()) by A19, Th5
.= Seg (len (WB .edgeSeq())) by FINSEQ_1:def 3 ;
consider n being odd Element of NAT such that
A27: n <= len WB and
A28: WB . n = W1 . (((2 * k) + 1) + 2) by A25, Lm45;
set W2 = WB9 .cut (1,n);
len (WB9 .cut (1,n)) = n by A27, Lm22;
then consider naa1 being even Element of NAT such that
A29: naa1 = n - 1 and
A30: len ((WB9 .cut (1,n)) .edgeSeq()) = naa1 div 2 by Lm42;
(2 * 0) + 1 <= n by ABIAN:12;
then A31: WB9 .cut (1,n) is_Walk_from W1 .first() ,W1 .last() by A4, A14, A27, A28, Lm16;
2 divides naa1 by PEPIN:22;
then A32: 2 * (naa1 div 2) = naa1 by NAT_D:3;

now :: thesis:

assume naa1 div 2 > len (WB .edgeSeq()) ; :: thesis:
then naa1 > 2 * (len (WB .edgeSeq())) by A32, XREAL_1:68;
then naa1 + 1 > (2 * (len (WB .edgeSeq()))) + 1 by XREAL_1:8;
hence contradiction by A27, A29, Def15; :: thesis:

end;

then Seg (naa1 div 2) c= dom (Sgm (dom esb)) by A26, FINSEQ_1:5;
then A33: dom ((Sgm (dom esb)) | (Seg (naa1 div 2))) = Seg (naa1 div 2) by RELAT_1:62;
reconsider ses = (Sgm (dom esb)) | (Seg (naa1 div 2)) as FinSequence ;
A34: ses is one-to-one by A24, FUNCT_1:52;
set es = esb | (rng ((Sgm (dom esb)) | (Seg (naa1 div 2))));
reconsider es = esb | (rng ((Sgm (dom esb)) | (Seg (naa1 div 2)))) as Subset of ((W1 .cut (1,((2 * k) + 1))) .edgeSeq()) by FINSEQ_6:153;
for x being object st x in es holds
x in W1 .edgeSeq() by A9, TARSKI:def 3;
then reconsider es = es as Subset of (W1 .edgeSeq()) by TARSKI:def 3;
reconsider esbes1 = esb \ es as Function ;

now :: thesis:

let z be object ; :: thesis:
A35: rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) c= rng (Sgm (dom esb)) by RELAT_1:70;
assume z in rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) ; :: thesis:
then z in rng (Sgm (dom esb)) by A35;
hence z in dom esb by FINSEQ_1:def 14; :: thesis:

end;

then rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) c= dom esb by TARSKI:def 3;
then A36: dom es = rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) by RELAT_1:62;

A37: now :: thesis:

let a, b be Nat; :: thesis:
assume that
A38: a in dom es and
A39: b in dom esbes1 ; :: thesis:
consider xa being object such that
A40: xa in dom ses and
A41: ses . xa = a by A36, A38, FUNCT_1:def 3;
reconsider xa = xa as Element of NAT by A40;
A42: xa in Seg (naa1 div 2) by A40, RELAT_1:57;
then A43: 1 <= xa by FINSEQ_1:1;
A44: [b,(esbes1 . b)] in esb \ es by A39, FUNCT_1:1;
then A45: [b,(esbes1 . b)] in esb by XBOOLE_0:def 5;
then b in dom esb by FUNCT_1:1;
then b in rng (Sgm (dom esb)) by FINSEQ_1:def 14;
then consider xb being object such that
A46: xb in dom (Sgm (dom esb)) and
A47: (Sgm (dom esb)) . xb = b by FUNCT_1:def 3;
reconsider xb = xb as Element of NAT by A46;
A48: 1 <= xb by A26, A46, FINSEQ_1:1;
A49: xa <= naa1 div 2 by A42, FINSEQ_1:1;

A50: now :: thesis:

assume xb <= xa ; :: thesis:
then xb <= naa1 div 2 by A49, XXREAL_0:2;
then A51: xb in Seg (naa1 div 2) by A48, FINSEQ_1:1;
[xb,b] in Sgm (dom esb) by A46, A47, FUNCT_1:1;
then [xb,b] in ses by A51, RELAT_1:def 11;
then b in rng ses by XTUPLE_0:def 13;
then [b,(esbes1 . b)] in es by A45, RELAT_1:def 11;
hence contradiction by A44, XBOOLE_0:def 5; :: thesis:

end;

xb <= len (WB .edgeSeq()) by A26, A46, FINSEQ_1:1;
then xb in dom (Seq esb) by A19, A48, FINSEQ_3:25;
then xb in dom (Sgm (dom esb)) by Th5;
then A52: xb <= len (Sgm (dom esb)) by FINSEQ_3:25;
a = (Sgm (dom esb)) . xa by A40, A41, FUNCT_1:47;
hence a < b by A47, A43, A52, A50, FINSEQ_1:def 14; :: thesis:

end;

len ses = naa1 div 2 by A33, FINSEQ_1:def 3;
then card (dom es) = naa1 div 2 by A36, A34, FINSEQ_4:62;
then card es = naa1 div 2 by CARD_1:62;
then A53: len (Seq es) = len ((WB9 .cut (1,n)) .edgeSeq()) by A30, Th4;
A54: es c= esb by RELAT_1:59;

now :: thesis:

let z be object ; :: thesis:

hereby :: thesis:

assume A55: z in esb ; :: thesis:

now :: thesis:

per cases ;

suppose z in es ; :: thesis:

hence z in es \/ (esb \ es) by XBOOLE_0:def 3; :: thesis:

end;

suppose not z in es ; :: thesis:

then z in esb \ es by A55, XBOOLE_0:def 5;
hence z in es \/ (esb \ es) by XBOOLE_0:def 3; :: thesis:

end;

hence z in es \/ (esb \ es) ; :: thesis:

end;

assume A56: z in es \/ (esb \ es) ; :: thesis:

now :: thesis:

per cases by A56, XBOOLE_0:def 3;

suppose z in es ; :: thesis:

hence z in esb by A54; :: thesis:

end;

suppose z in esb \ es ; :: thesis:

hence z in esb by XBOOLE_0:def 5; :: thesis:

end;

hence z in esb ; :: thesis:

end;

then esb = es \/ (esb \ es) by TARSKI:2;
then A57: dom esb = (dom es) \/ (dom (esb \ es)) by XTUPLE_0:23;
A59: Sgm (dom esb) = (Sgm (dom es)) ^ (Sgm (dom (esb \ es))) by A57, A37, FINSEQ_3:42;
A60: (WB9 .cut (1,n)) .edgeSeq() c= WB .edgeSeq() by Lm43;
then A61: dom ((WB9 .cut (1,n)) .edgeSeq()) c= dom (Seq esb) by A19, RELAT_1:11;
A62: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 15;

now :: thesis:

end;

then (WB9 .cut (1,n)) .edgeSeq() = Seq es by A53, FINSEQ_1:14;
then reconsider W2 = WB9 .cut (1,n) as Path of W1 by A31, Def32;
take W2 = W2; :: thesis:
thus W2 is directed ; :: thesis:

end;

suppose A71: not W1 . (((2 * k) + 1) + 2) in WB .vertices() ; :: thesis:

set es = esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)));
set W2 = WB .addEdge (W1 . (((2 * k) + 1) + 1));

A72: now :: thesis:

let m, n be Nat; :: thesis:
assume that
A73: m in dom esb and
A74: n in {(k + 1)} ; :: thesis:
A75: n = k + 1 by A74, TARSKI:def 1;
m <= k by A23, A73, FINSEQ_1:1;
hence m < n by A75, NAT_1:13; :: thesis:

end;

A76: dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) = {(k + 1)} ;
then A77: dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) = (dom esb) \/ {(k + 1)} by FUNCT_4:def 1;

now :: thesis:

let x be object ; :: thesis:
assume A78: x in dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) ; :: thesis:

now :: thesis:

per cases by A77, A78, XBOOLE_0:def 3;

suppose x in dom esb ; :: thesis:

then A79: x in Seg k by A22;
then reconsider x9 = x as Element of NAT ;
x9 <= k by A79, FINSEQ_1:1;
then A80: x9 <= k + 1 by NAT_1:12;
1 <= x9 by A79, FINSEQ_1:1;
hence x in Seg (k + 1) by A80, FINSEQ_1:1; :: thesis:

end;

suppose A81: x in {(k + 1)} ; :: thesis:

A82: 1 <= k + 1 by NAT_1:12;
x = k + 1 by A81, TARSKI:def 1;
hence x in Seg (k + 1) by A82, FINSEQ_1:1; :: thesis:

end;

hence x in Seg (k + 1) ; :: thesis:

end;

then dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) c= Seg (k + 1) by TARSKI:def 3;
then reconsider es = esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) as FinSubsequence by FINSEQ_1:def 12;

now :: thesis:

let z be object ; :: thesis:
assume A84: z in es ; :: thesis:
then consider x, y being object such that
A85: z = [x,y] by RELAT_1:def 1;
A86: x in dom es by A84, A85, FUNCT_1:1;
A87: es . x = y by A84, A85, FUNCT_1:1;

now :: thesis:

per cases ;

suppose A88: x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) ; :: thesis:

then reconsider x9 = x as Element of NAT by A76;
A89: x = k + 1 by A88, TARSKI:def 1;
then A90: 1 <= x9 by NAT_1:12;
then A91: x in dom (W1 .edgeSeq()) by A3, A89, FINSEQ_3:25;
y = ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) . x by A77, A86, A87, A88, FUNCT_4:def 1;
then A92: y = W1 . (((2 * k) + 1) + 1) by A89, FUNCOP_1:72;
(W1 .edgeSeq()) . x = W1 . (2 * (k + 1)) by A3, A89, A90, Def15
.= W1 . (((2 * k) + 1) + 1) ;
hence z in W1 .edgeSeq() by A85, A92, A91, FUNCT_1:1; :: thesis:

end;

suppose A93: not x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) ; :: thesis:

then A94: x in dom esb by A77, A86, XBOOLE_0:def 3;
y = esb . x by A77, A86, A87, A93, FUNCT_4:def 1;
then [x,y] in esb by A94, FUNCT_1:1;
then [x,y] in (W1 .cut (1,((2 * k) + 1))) .edgeSeq() ;
hence z in W1 .edgeSeq() by A9, A85; :: thesis:

end;

hence z in W1 .edgeSeq() ; :: thesis:

end;

then reconsider es = es as Subset of (W1 .edgeSeq()) by TARSKI:def 3;
A95: Sgm (dom es) = (Sgm (dom esb)) ^ (Sgm {(k + 1)}) by A77, A72, FINSEQ_3:42
.= (Sgm (dom esb)) ^ <*(k + 1)*> by FINSEQ_3:44 ;

now :: thesis:

assume (dom esb) /\ (dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) <> {} ; :: thesis:
then consider x being object such that
A96: x in (dom esb) /\ (dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) by XBOOLE_0:def 1;
x in {(k + 1)} by A96;
then A97: x = k + 1 by TARSKI:def 1;
x in dom esb by A96, XBOOLE_0:def 4;
then k + 1 <= k + 0 by A23, A97, FINSEQ_1:1;
hence contradiction by XREAL_1:6; :: thesis:

end;

then A98: dom esb misses dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) by XBOOLE_0:def 7;
A99: (WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq() = (Seq esb) ^ <*(W1 . (((2 * k) + 1) + 1))*> by A16, A19, Lm44;
then A100: len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) = (len (Seq esb)) + (len <*(W1 . (((2 * k) + 1) + 1))*>) by FINSEQ_1:22
.= (len (Seq esb)) + 1 by FINSEQ_1:39
.= (card esb) + 1 by Th4 ;
A101: len (Seq es) = card es by Th4
.= (card esb) + (card ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) by A98, PRE_CIRC:22
.= (card esb) + (card {[(k + 1),(W1 . (((2 * k) + 1) + 1))]}) by FUNCT_4:82
.= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) by A100, CARD_1:30 ;

now :: thesis:

A102: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 15;
let n be Nat; :: thesis:
assume that
A103: 1 <= n and
A104: n <= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) ; :: thesis:
n in dom (Seq es) by A101, A103, A104, FINSEQ_3:25;
then A105: (Seq es) . n = es . ((Sgm (dom es)) . n) by A102, FUNCT_1:12;
A106: Seq esb = esb * (Sgm (dom esb)) by FINSEQ_1:def 15;
A107: n in dom ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) by A103, A104, FINSEQ_3:25;

now :: thesis:

per cases by A99, A107, FINSEQ_1:25;

suppose A108: n in dom (Seq esb) ; :: thesis:

then n in dom (Sgm (dom esb)) by A106, FUNCT_1:11;
then A109: (Sgm (dom es)) . n = (Sgm (dom esb)) . n by A95, FINSEQ_1:def 7;
A110: (Sgm (dom esb)) . n in dom esb by A106, A108, FUNCT_1:11;
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq esb) . n by A99, A108, FINSEQ_1:def 7
.= esb . ((Sgm (dom esb)) . n) by A106, A108, FUNCT_1:12 ;
hence ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n by A98, A105, A110, A109, FUNCT_4:16; :: thesis:

end;

suppose ex m being Nat st
( m in dom <*(W1 . (((2 * k) + 1) + 1))*> & n = (len (Seq esb)) + m ) ; :: thesis:

then consider m being Nat such that
A111: m in dom <*(W1 . (((2 * k) + 1) + 1))*> and
A112: n = (len (Seq esb)) + m ;
m in {1} by A111, FINSEQ_1:2, FINSEQ_1:def 8;
then A113: m = 1 by TARSKI:def 1;
A114: k + 1 in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) by TARSKI:def 1;
then A115: k + 1 in (dom esb) \/ (dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) by XBOOLE_0:def 3;
len (Sgm (dom esb)) = card (dom esb) by FINSEQ_3:39
.= card esb by CARD_1:62
.= len (Seq esb) by Th4 ;
then (Seq es) . n = es . (k + 1) by A95, A105, A112, A113, FINSEQ_1:42;
then A116: (Seq es) . n = ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) . (k + 1) by A114, A115, FUNCT_4:def 1
.= W1 . (((2 * k) + 1) + 1) by FUNCOP_1:72 ;
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = <*(W1 . (((2 * k) + 1) + 1))*> . 1 by A99, A111, A112, A113, FINSEQ_1:def 7
.= W1 . (((2 * k) + 1) + 1) ;
hence ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n by A116; :: thesis:

end;

hence ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n ; :: thesis:

end;

then A117: (WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq() = Seq es by A101, FINSEQ_1:14;
WB .addEdge (W1 . (((2 * k) + 1) + 1)) is_Walk_from W1 .first() ,W1 .last() by A4, A8, A6, A10, A13, A12, Lm52;
then reconsider W2 = WB .addEdge (W1 . (((2 * k) + 1) + 1)) as Path of W1 by A16, A18, A71, A117, Def32, Lm68;
take W2 = W2; :: thesis:
thus W2 is directed by A8, A6, A10, A12, Lm52; :: thesis:

end;

hence ex W2 being Path of W1 st W2 is directed ; :: thesis:

end;

hence ex W2 being Path of W1 st W2 is directed ; :: thesis:

end;

then A118: for k being Nat st S₁[k] holds
S₁[k + 1] ;

now :: thesis:

let W1 be DWalk of G; :: thesis:
set W2 = the Path of W1;
assume W1 .length() = 0 ; :: thesis:
then len W1 = (2 * 0) + 1 by Def15;
then A119: len the Path of W1 <= 1 by Lm72;
take W2 = the Path of W1; :: thesis:
1 <= len W2 by ABIAN:12;
then len W2 = 1 by A119, XXREAL_0:1;
then W2 is trivial by Lm55;
then ex v being Vertex of G st W2 = G .walkOf v by Lm56;
hence W2 is directed ; :: thesis:

end;

then A120: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A120, A118);
hence ex b₁ being Path of W st b₁ is directed by A1; :: thesis: