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 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
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 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;
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;
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 A7, FINSEQ_1:def 3; :: 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 A21, A20, FUNCT_1:26;
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 (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 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: 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 A23, FINSEQ_1:def 13; :: 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 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;
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 A23, A47, A43, A52, A50, FINSEQ_1:def 13; :: thesis: verum
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: 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 A55, XBOOLE_0:def 5;
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 A56, XBOOLE_0:def 3;
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 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
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;
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: 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 A74, TARSKI:def 1;
m <= k by A23, A73, FINSEQ_1:1;
hence m < n by A75, NAT_1:13; :: 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 A77, A78, XBOOLE_0:def 3;
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;
suppose A81: x in {(k + 1)} ; :: thesis: x in Seg (k + 1)
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: 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 A84, A85, FUNCT_1:1;
A87: es . x = y by A84, A85, FUNCT_1:1;
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 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;
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;
end;
end;
hence z in W1 .edgeSeq() ; :: thesis: verum
end;
then reconsider es = es as Subset of (W1 .edgeSeq()) by TARSKI:def 3;
{(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)))) <> {}
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 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: 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 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) . 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 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;
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 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;
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 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: 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 A119, XXREAL_0:1;
then W2 is V5() 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 NAT_1:sch 2(A120, A118);
 hence ex b1 being Path of W st b1 is directed by A1; :: thesis: verum