defpred S_{1}[ 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() ;

_{1}[k] holds

S_{1}[k + 1]
;

_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A120, A118);

hence ex b_{1} being Path of W st b_{1} is directed
by A1; :: thesis: verum

ex W2 being Path of W1 st W2 is directed ;

A1: W .length() = W .length() ;

now :: thesis: for k being Nat st S_{1}[k] holds

for W1 being DWalk of G st W1 .length() = k + 1 holds

ex W2 being Path of W1 st W2 is directed

then A118:
for k being Nat st Sfor 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: ( S_{1}[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: S_{1}[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 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;

end;ex W2 being Path of W1 st W2 is directed )

assume A2: S

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 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;

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

hence
ex W2 being Path of W1 st W2 is directed
; :: thesis: verumper cases
( WB is closed or WB is open )
;

end;

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 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: W2 is directed

thus W2 is directed ; :: thesis: verum

end;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: W2 is directed

thus W2 is directed ; :: thesis: verum

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 A19, Def27;

A21: Seq esb = esb * (Sgm (dom esb)) by FINSEQ_1:def 14;

then rng (Sgm (dom esb)) = dom esb by FINSEQ_1:def 13;

then A24: Sgm (dom esb) is one-to-one by A21, A20, FUNCT_1:26;

end;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 14;

A22: now :: thesis: for x being object st x in dom esb holds

x in Seg k

then A23:
dom esb c= Seg k
by TARSKI:def 3;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 A7, FINSEQ_1:def 3; :: thesis: verum

end;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 A7, FINSEQ_1:def 3; :: thesis: verum

then rng (Sgm (dom esb)) = dom esb by FINSEQ_1:def 13;

then A24: Sgm (dom esb) is one-to-one by A21, A20, FUNCT_1:26;

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

hence
ex W2 being Path of W1 st W2 is directed
; :: thesis: verumper cases
( W1 . (((2 * k) + 1) + 2) in WB .vertices() or not W1 . (((2 * k) + 1) + 2) in WB .vertices() )
;

end;

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 (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;

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 ;

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

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;

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 A23, XBOOLE_1:1;

dom es c= dom esb by A54, RELAT_1:11;

then dom es c= Seg k by A23, XBOOLE_1:1;

then A59: Sgm (dom esb) = (Sgm (dom es)) ^ (Sgm (dom (esb \ es))) by A57, A58, 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 14;

then reconsider W2 = WB9 .cut (1,n) as Path of W1 by A31, Def32;

take W2 = W2; :: thesis: W2 is directed

thus W2 is directed ; :: thesis: verum

end;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: not naa1 div 2 > len (WB .edgeSeq())

then
Seg (naa1 div 2) c= dom (Sgm (dom esb))
by A26, FINSEQ_1:5;assume
naa1 div 2 > len (WB .edgeSeq())
; :: thesis: contradiction

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: verum

end;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: verum

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: for z being object st z in rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) holds

z in dom esb

then
rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) c= dom esb
by TARSKI:def 3;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 A23, FINSEQ_1:def 13; :: thesis: verum

end;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 A23, FINSEQ_1:def 13; :: thesis: verum

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

len ses = naa1 div 2
by A33, FINSEQ_1:def 3;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 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 A23, FINSEQ_1:def 13;

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;

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 A23, A47, A43, A52, A50, FINSEQ_1:def 13; :: thesis: verum

end;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 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 A23, FINSEQ_1:def 13;

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: not xb <= xa

xb <= len (WB .edgeSeq())
by A26, A46, FINSEQ_1:1;assume
xb <= xa
; :: thesis: contradiction

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: verum

end;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: verum

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 A23, A47, A43, A52, A50, FINSEQ_1:def 13; :: thesis: verum

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: for z being object holds

( ( z in esb implies z in es \/ (esb \ es) ) & ( z in es \/ (esb \ es) implies z in esb ) )

then
esb = es \/ (esb \ es)
by TARSKI:2;( ( 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 ) )

hence z in esb ; :: thesis: verum

end;hereby :: thesis: ( z in es \/ (esb \ es) implies z in esb )

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

end;now :: thesis: z in es \/ (esb \ es)

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

hence z in esb ; :: thesis: verum

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 A23, XBOOLE_1:1;

dom es c= dom esb by A54, RELAT_1:11;

then dom es c= Seg k by A23, XBOOLE_1:1;

then A59: Sgm (dom esb) = (Sgm (dom es)) ^ (Sgm (dom (esb \ es))) by A57, A58, 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 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

then
(WB9 .cut (1,n)) .edgeSeq() = Seq es
by A53, FINSEQ_1:14;((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 A63, A64, FINSEQ_3:25;

then x in dom (Sgm (dom esb)) by A21, A61, FUNCT_1:11;

then A66: [x,((Sgm (dom esb)) . x)] in Sgm (dom esb) by FUNCT_1:1;

x in Seg (naa1 div 2) by A30, A63, A64, FINSEQ_1:1;

then [x,((Sgm (dom esb)) . x)] in ses by A66, RELAT_1:def 11;

then A67: (Sgm (dom esb)) . x in rng ses by XTUPLE_0:def 13;

(Sgm (dom esb)) . x in dom esb by A21, A61, A65, FUNCT_1:11;

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 A67, RELAT_1:def 11;

[x,(((WB9 .cut (1,n)) .edgeSeq()) . x)] in (WB9 .cut (1,n)) .edgeSeq() by A65, FUNCT_1:1;

then A69: ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq esb) . x by A19, A60, FUNCT_1:1

.= esb . ((Sgm (dom esb)) . x) by A21, A61, A65, FUNCT_1:12 ;

A70: x in dom (Seq es) by A53, A63, A64, FINSEQ_3:25;

then x in dom (Sgm (dom es)) by Th5;

then (Sgm (dom esb)) . x = (Sgm (dom es)) . x by A59, FINSEQ_1:def 7;

then es . ((Sgm (dom es)) . x) = esb . ((Sgm (dom esb)) . x) by A68, FUNCT_1:1;

hence ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . x by A62, A69, A70, FUNCT_1:12; :: thesis: verum

end;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 A63, A64, FINSEQ_3:25;

then x in dom (Sgm (dom esb)) by A21, A61, FUNCT_1:11;

then A66: [x,((Sgm (dom esb)) . x)] in Sgm (dom esb) by FUNCT_1:1;

x in Seg (naa1 div 2) by A30, A63, A64, FINSEQ_1:1;

then [x,((Sgm (dom esb)) . x)] in ses by A66, RELAT_1:def 11;

then A67: (Sgm (dom esb)) . x in rng ses by XTUPLE_0:def 13;

(Sgm (dom esb)) . x in dom esb by A21, A61, A65, FUNCT_1:11;

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 A67, RELAT_1:def 11;

[x,(((WB9 .cut (1,n)) .edgeSeq()) . x)] in (WB9 .cut (1,n)) .edgeSeq() by A65, FUNCT_1:1;

then A69: ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq esb) . x by A19, A60, FUNCT_1:1

.= esb . ((Sgm (dom esb)) . x) by A21, A61, A65, FUNCT_1:12 ;

A70: x in dom (Seq es) by A53, A63, A64, FINSEQ_3:25;

then x in dom (Sgm (dom es)) by Th5;

then (Sgm (dom esb)) . x = (Sgm (dom es)) . x by A59, FINSEQ_1:def 7;

then es . ((Sgm (dom es)) . x) = esb . ((Sgm (dom esb)) . x) by A68, FUNCT_1:1;

hence ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . x by A62, A69, A70, FUNCT_1:12; :: thesis: verum

then reconsider W2 = WB9 .cut (1,n) as Path of W1 by A31, Def32;

take W2 = W2; :: thesis: W2 is directed

thus W2 is directed ; :: thesis: verum

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));

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

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

{(k + 1)} c= Seg (k + 1) by A77, A83, XBOOLE_1:11;

then A95: Sgm (dom es) = (Sgm (dom esb)) ^ (Sgm {(k + 1)}) by A23, A77, A72, FINSEQ_3:42

.= (Sgm (dom esb)) ^ <*(k + 1)*> by FINSEQ_3:44 ;

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 ;

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: W2 is directed

thus W2 is directed by A8, A6, A10, A12, Lm52; :: thesis: verum

end;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

A76:
dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) = {(k + 1)}
;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 A74, TARSKI:def 1;

m <= k by A23, A73, FINSEQ_1:1;

hence m < n by A75, NAT_1:13; :: thesis: verum

end;assume that

A73: m in dom esb and

A74: n in {(k + 1)} ; :: thesis: m < n

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: verum

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)

then A83:
dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) c= Seg (k + 1)
by TARSKI:def 3;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)

end;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)end;

hence
x in Seg (k + 1)
; :: thesis: verumper cases
( x in dom esb or x in {(k + 1)} )
by A77, A78, XBOOLE_0:def 3;

end;

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 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: verum

end;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: verum

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()

then reconsider es = es as Subset of (W1 .edgeSeq()) by TARSKI:def 3;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 A84, A85, FUNCT_1:1;

A87: es . x = y by A84, A85, FUNCT_1:1;

end;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 A84, A85, FUNCT_1:1;

A87: es . x = y by A84, A85, FUNCT_1:1;

now :: thesis: z in W1 .edgeSeq() end;

hence
z in W1 .edgeSeq()
; :: thesis: verumper cases
( x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) or not x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) )
;

end;

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 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: verum

end;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: verum

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 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: verum

end;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: verum

{(k + 1)} c= Seg (k + 1) by A77, A83, XBOOLE_1:11;

then A95: Sgm (dom es) = (Sgm (dom esb)) ^ (Sgm {(k + 1)}) by A23, A77, A72, FINSEQ_3:42

.= (Sgm (dom esb)) ^ <*(k + 1)*> by FINSEQ_3:44 ;

now :: thesis: not (dom esb) /\ (dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) <> {}

then A98:
dom esb misses dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))
by XBOOLE_0:def 7;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 A96, XBOOLE_0:def 4;

then k + 1 <= k + 0 by A23, A97, FINSEQ_1:1;

hence contradiction by XREAL_1:6; :: thesis: verum

end;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: verum

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: 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

then A117:
(WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq() = Seq es
by A101, FINSEQ_1:14;((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 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 14;

A107: n in dom ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) by A103, A104, FINSEQ_3:25;

end;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 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 14;

A107: n in dom ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) by A103, A104, FINSEQ_3:25;

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

hence
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
; :: thesis: verumper 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 A99, A107, FINSEQ_1:25;

end;

( m in dom <*(W1 . (((2 * k) + 1) + 1))*> & n = (len (Seq esb)) + m ) ) by A99, A107, FINSEQ_1:25;

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 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: verum

end;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: verum

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

( 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 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 A23, 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) by FINSEQ_1:def 8 ;

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

end;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 A23, 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) by FINSEQ_1:def 8 ;

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

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: W2 is directed

thus W2 is directed by A8, A6, A10, A12, Lm52; :: thesis: verum

S

now :: thesis: for W1 being DWalk of G st W1 .length() = 0 holds

ex W2 being Path of W1 st W2 is directed

then A120:
Sex 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 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: verum

end;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 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: verum

for k being Nat holds S

hence ex b