defpred S1[ 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() ;
now :: thesis: for k being Nat st S1[k] holds
for W1 being DWalk of G st W1 .length() = k + 1 holds
ex W2 being Path of W1 st W2 is directed
let k be Nat; :: thesis: ( S1[k] implies for W1 being DWalk of G st W1 .length() = k + 1 holds
ex W2 being Path of W1 st W2 is directed )

assume A2: S1[k] ; :: thesis: for W1 being DWalk of G st W1 .length() = k + 1 holds
ex W2 being Path of W1 st W2 is directed

let W1 be DWalk of G; :: thesis: ( W1 .length() = k + 1 implies ex W2 being Path of W1 st W2 is directed )
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: ex W2 being Path of W1 st W2 is directed
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 ;
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 ;
A13: (W1 .cut (1,((2 * k) + 1))) .first() = W1 . 1 by ;
then A14: WB .first() = W1 . 1 by A10;
A15: WB .last() = W1 . ((2 * k) + 1) by ;
then A16: W1 . (((2 * k) + 1) + 1) Joins WB .last() ,W1 . (((2 * k) + 1) + 2),G by ;
now :: thesis: ex W2 being Path of W1 st W2 is directed
per cases ( WB is closed or WB is open ) ;
suppose A17: WB is closed ; :: thesis: ex W2 being Path of W1 st W2 is directed
set W2 = W1 .remove (1,((2 * k) + 1));
W1 .first() = W1 . ((2 * k) + 1) by ;
then W1 .remove (1,((2 * k) + 1)) = W1 .cut (((2 * k) + 1),(((2 * k) + 1) + 2)) by ;
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: W2 is directed
thus W2 is directed ; :: thesis: verum
end;
suppose A18: WB is open ; :: thesis: ex W2 being Path of W1 st W2 is directed
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 ;
A21: Seq esb = esb * (Sgm (dom esb)) by FINSEQ_1:def 14;
A22: now :: thesis: for x being object st x in dom esb holds
x in Seg k
let x be object ; :: thesis: ( x in dom esb implies x in Seg k )
assume x in dom esb ; :: thesis: x in Seg k
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 ; :: thesis: verum
end;
then A23: dom esb c= Seg k by TARSKI:def 3;
then rng (Sgm (dom esb)) = dom esb by FINSEQ_1:def 13;
then A24: Sgm (dom esb) is one-to-one by ;
now :: thesis: ex W2 being Path of W1 st W2 is directed
per cases ( W1 . (((2 * k) + 1) + 2) in WB .vertices() or not W1 . (((2 * k) + 1) + 2) in WB .vertices() ) ;
suppose A25: W1 . (((2 * k) + 1) + 2) in WB .vertices() ; :: thesis: ex W2 being Path of W1 st W2 is directed
reconsider WB9 = WB as directed Path of G by A8;
A26: dom (Sgm (dom esb)) = dom () by
.= Seg (len ()) 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 ;
set W2 = WB9 .cut (1,n);
len (WB9 .cut (1,n)) = n by ;
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: not naa1 div 2 > len ()
assume naa1 div 2 > len () ; :: thesis: contradiction
then naa1 > 2 * (len ()) by ;
then naa1 + 1 > (2 * (len ())) + 1 by XREAL_1:8;
hence contradiction by A27, A29, Def15; :: thesis: verum
end;
then Seg (naa1 div 2) c= dom (Sgm (dom esb)) by ;
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 ;
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 ;
then reconsider es = es as Subset of () by TARSKI:def 3;
reconsider esbes1 = esb \ es as Function ;
now :: thesis: for z being object st z in rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) holds
z in dom esb
let z be object ; :: thesis: ( z in rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) implies z in dom esb )
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: z in dom esb
then z in rng (Sgm (dom esb)) by A35;
hence z in dom esb by ; :: thesis: verum
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: for a, b being Nat st a in dom es & b in dom esbes1 holds
a < b
let a, b be Nat; :: thesis: ( a in dom es & b in dom esbes1 implies a < b )
assume that
A38: a in dom es and
A39: b in dom esbes1 ; :: thesis: a < b
consider xa being object such that
A40: xa in dom ses and
A41: ses . xa = a by ;
reconsider xa = xa as Element of NAT by A40;
A42: xa in Seg (naa1 div 2) by ;
then A43: 1 <= xa by FINSEQ_1:1;
A44: [b,(esbes1 . b)] in esb \ es by ;
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 ;
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 ;
A49: xa <= naa1 div 2 by ;
A50: now :: thesis: not xb <= xa
assume xb <= xa ; :: thesis: contradiction
then xb <= naa1 div 2 by ;
then A51: xb in Seg (naa1 div 2) by ;
[xb,b] in Sgm (dom esb) by ;
then [xb,b] in ses by ;
then b in rng ses by XTUPLE_0:def 13;
then [b,(esbes1 . b)] in es by ;
hence contradiction by A44, XBOOLE_0:def 5; :: thesis: verum
end;
xb <= len () by ;
then xb in dom (Seq esb) by ;
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 ;
hence a < b by ; :: thesis: verum
end;
len ses = naa1 div 2 by ;
then card (dom es) = naa1 div 2 by ;
then card es = naa1 div 2 by CARD_1:62;
then A53: len (Seq es) = len ((WB9 .cut (1,n)) .edgeSeq()) by ;
A54: es c= esb by RELAT_1:59;
now :: thesis: for z being object holds
( ( z in esb implies z in es \/ (esb \ es) ) & ( z in es \/ (esb \ es) implies z in esb ) )
let z be object ; :: thesis: ( ( z in esb implies z in es \/ (esb \ es) ) & ( z in es \/ (esb \ es) implies z in esb ) )
hereby :: thesis: ( z in es \/ (esb \ es) implies z in esb )
assume A55: z in esb ; :: thesis: z in es \/ (esb \ es)
now :: thesis: z in es \/ (esb \ es)
per cases ( z in es or not z in es ) ;
suppose z in es ; :: thesis: z in es \/ (esb \ es)
hence z in es \/ (esb \ es) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose not z in es ; :: thesis: z in es \/ (esb \ es)
then z in esb \ es by ;
hence z in es \/ (esb \ es) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence z in es \/ (esb \ es) ; :: thesis: verum
end;
assume A56: z in es \/ (esb \ es) ; :: thesis: z in esb
now :: thesis: z in esb
per cases ( z in es or z in esb \ es ) by ;
suppose z in es ; :: thesis: z in esb
hence z in esb by A54; :: thesis: verum
end;
suppose z in esb \ es ; :: thesis: z in esb
hence z in esb by XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
hence z in esb ; :: thesis: verum
end;
then esb = es \/ (esb \ es) by TARSKI:2;
then A57: dom esb = (dom es) \/ (dom (esb \ es)) by XTUPLE_0:23;
esb \ es c= esb by XBOOLE_1:36;
then dom (esb \ es) c= dom esb by RELAT_1:11;
then A58: dom (esb \ es) c= Seg k by ;
dom es c= dom esb by ;
then dom es c= Seg k by ;
then A59: Sgm (dom esb) = (Sgm (dom es)) ^ (Sgm (dom (esb \ es))) by ;
A60: (WB9 .cut (1,n)) .edgeSeq() c= WB .edgeSeq() by Lm43;
then A61: dom ((WB9 .cut (1,n)) .edgeSeq()) c= dom (Seq esb) by ;
A62: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 14;
now :: thesis: for x being Nat st 1 <= x & x <= len ((WB9 .cut (1,n)) .edgeSeq()) holds
((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . x
let x be Nat; :: thesis: ( 1 <= x & x <= len ((WB9 .cut (1,n)) .edgeSeq()) implies ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . x )
assume that
A63: 1 <= x and
A64: x <= len ((WB9 .cut (1,n)) .edgeSeq()) ; :: thesis: ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . x
A65: x in dom ((WB9 .cut (1,n)) .edgeSeq()) by ;
then x in dom (Sgm (dom esb)) by ;
then A66: [x,((Sgm (dom esb)) . x)] in Sgm (dom esb) by FUNCT_1:1;
x in Seg (naa1 div 2) by ;
then [x,((Sgm (dom esb)) . x)] in ses by ;
then A67: (Sgm (dom esb)) . x in rng ses by XTUPLE_0:def 13;
(Sgm (dom esb)) . x in dom esb by ;
then [((Sgm (dom esb)) . x),(esb . ((Sgm (dom esb)) . x))] in esb by FUNCT_1:1;
then A68: [((Sgm (dom esb)) . x),(esb . ((Sgm (dom esb)) . x))] in es by ;
[x,(((WB9 .cut (1,n)) .edgeSeq()) . x)] in (WB9 .cut (1,n)) .edgeSeq() by ;
then A69: ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq esb) . x by
.= esb . ((Sgm (dom esb)) . x) by ;
A70: x in dom (Seq es) by ;
then x in dom (Sgm (dom es)) by Th5;
then (Sgm (dom esb)) . x = (Sgm (dom es)) . x by ;
then es . ((Sgm (dom es)) . x) = esb . ((Sgm (dom esb)) . x) by ;
hence ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . x by ; :: thesis: verum
end;
then (WB9 .cut (1,n)) .edgeSeq() = Seq es by ;
then reconsider W2 = WB9 .cut (1,n) as Path of W1 by ;
take W2 = W2; :: thesis: W2 is directed
thus W2 is directed ; :: thesis: verum
end;
suppose A71: not W1 . (((2 * k) + 1) + 2) in WB .vertices() ; :: thesis: ex W2 being Path of W1 st W2 is directed
set es = esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)));
set W2 = WB .addEdge (W1 . (((2 * k) + 1) + 1));
A72: now :: thesis: for m, n being Nat st m in dom esb & n in {(k + 1)} holds
m < n
let m, n be Nat; :: thesis: ( m in dom esb & n in {(k + 1)} implies m < n )
assume that
A73: m in dom esb and
A74: n in {(k + 1)} ; :: thesis: m < n
A75: n = k + 1 by ;
m <= k by ;
hence m < n by ; :: thesis: verum
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: for x being object st x in dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) holds
x in Seg (k + 1)
let x be object ; :: thesis: ( x in dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) implies x in Seg (k + 1) )
assume A78: x in dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) ; :: thesis: x in Seg (k + 1)
now :: thesis: x in Seg (k + 1)
per cases ( x in dom esb or x in {(k + 1)} ) by ;
suppose x in dom esb ; :: thesis: x in Seg (k + 1)
then A79: x in Seg k by A22;
then reconsider x9 = x as Element of NAT ;
x9 <= k by ;
then A80: x9 <= k + 1 by NAT_1:12;
1 <= x9 by ;
hence x in Seg (k + 1) by ; :: thesis: verum
end;
suppose A81: x in {(k + 1)} ; :: thesis: x in Seg (k + 1)
A82: 1 <= k + 1 by NAT_1:12;
x = k + 1 by ;
hence x in Seg (k + 1) by ; :: thesis: verum
end;
end;
end;
hence x in Seg (k + 1) ; :: thesis: verum
end;
then A83: 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: for z being object st z in es holds
z in W1 .edgeSeq()
let z be object ; :: thesis: ( z in es implies z in W1 .edgeSeq() )
assume A84: z in es ; :: thesis: z in W1 .edgeSeq()
then consider x, y being object such that
A85: z = [x,y] by RELAT_1:def 1;
A86: x in dom es by ;
A87: es . x = y by ;
now :: thesis: z in W1 .edgeSeq()
per cases ( x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) or not x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) ) ;
suppose A88: x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) ; :: thesis: z in W1 .edgeSeq()
then reconsider x9 = x as Element of NAT by A76;
A89: x = k + 1 by ;
then A90: 1 <= x9 by NAT_1:12;
then A91: x in dom () by ;
y = ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) . x by ;
then A92: y = W1 . (((2 * k) + 1) + 1) by ;
() . x = W1 . (2 * (k + 1)) by
.= W1 . (((2 * k) + 1) + 1) ;
hence z in W1 .edgeSeq() by ; :: thesis: verum
end;
suppose A93: not x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) ; :: thesis: z in W1 .edgeSeq()
then A94: x in dom esb by ;
y = esb . x by ;
then [x,y] in esb by ;
then [x,y] in (W1 .cut (1,((2 * k) + 1))) .edgeSeq() ;
hence z in W1 .edgeSeq() by ; :: thesis: verum
end;
end;
end;
hence z in W1 .edgeSeq() ; :: thesis: verum
end;
then reconsider es = es as Subset of () by TARSKI:def 3;
{(k + 1)} c= Seg (k + 1) by ;
then A95: Sgm (dom es) = (Sgm (dom esb)) ^ (Sgm {(k + 1)}) by
.= (Sgm (dom esb)) ^ <*(k + 1)*> by FINSEQ_3:44 ;
now :: thesis: not (dom esb) /\ (dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) <> {}
assume (dom esb) /\ (dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) <> {} ; :: thesis: contradiction
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 ;
then k + 1 <= k + 0 by ;
hence contradiction by XREAL_1:6; :: thesis: verum
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 ;
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
.= (card esb) + (card {[(k + 1),(W1 . (((2 * k) + 1) + 1))]}) by FUNCT_4:82
.= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) by ;
now :: thesis: for n being Nat st 1 <= n & n <= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) holds
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
A102: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 14;
let n be Nat; :: thesis: ( 1 <= n & n <= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) implies ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n )
assume that
A103: 1 <= n and
A104: n <= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) ; :: thesis: ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
n in dom (Seq es) by ;
then A105: (Seq es) . n = es . ((Sgm (dom es)) . n) by ;
A106: Seq esb = esb * (Sgm (dom esb)) by FINSEQ_1:def 14;
A107: n in dom ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) by ;
now :: thesis: ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
per cases ( n in dom (Seq esb) or ex m being Nat st
( m in dom <*(W1 . (((2 * k) + 1) + 1))*> & n = (len (Seq esb)) + m ) )
by ;
suppose A108: n in dom (Seq esb) ; :: thesis: ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
then n in dom (Sgm (dom esb)) by ;
then A109: (Sgm (dom es)) . n = (Sgm (dom esb)) . n by ;
A110: (Sgm (dom esb)) . n in dom esb by ;
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq esb) . n by
.= esb . ((Sgm (dom esb)) . n) by ;
hence ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n by ; :: thesis: verum
end;
suppose ex m being Nat st
( m in dom <*(W1 . (((2 * k) + 1) + 1))*> & n = (len (Seq esb)) + m ) ; :: thesis: ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
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 ;
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
.= card esb by CARD_1:62
.= len (Seq esb) by Th4 ;
then (Seq es) . n = es . (k + 1) by ;
then A116: (Seq es) . n = ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) . (k + 1) by
.= 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
.= W1 . (((2 * k) + 1) + 1) by FINSEQ_1:def 8 ;
hence ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n by A116; :: thesis: verum
end;
end;
end;
hence ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n ; :: thesis: verum
end;
then A117: (WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq() = Seq es by ;
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 ;
take W2 = W2; :: thesis: W2 is directed
thus W2 is directed by A8, A6, A10, A12, Lm52; :: thesis: verum
end;
end;
end;
hence ex W2 being Path of W1 st W2 is directed ; :: thesis: verum
end;
end;
end;
hence ex W2 being Path of W1 st W2 is directed ; :: thesis: verum
end;
then A118: for k being Nat st S1[k] holds
S1[k + 1] ;
now :: thesis: for W1 being DWalk of G st W1 .length() = 0 holds
ex W2 being Path of W1 st W2 is directed
let W1 be DWalk of G; :: thesis: ( W1 .length() = 0 implies ex W2 being Path of W1 st W2 is directed )
set W2 = the Path of W1;
assume W1 .length() = 0 ; :: thesis: ex W2 being Path of W1 st W2 is directed
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: W2 is directed
1 <= len W2 by ABIAN:12;
then len W2 = 1 by ;
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: verum
end;
then A120: S1[ 0 ] ;
for k being Nat holds S1[k] from hence ex b1 being Path of W st b1 is directed by A1; :: thesis: verum