let G be _Graph; :: thesis: for W being vertex-distinct Walk of G

for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds

W .addEdge e is vertex-distinct

let W be vertex-distinct Walk of G; :: thesis: for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds

W .addEdge e is vertex-distinct

let e, v be object ; :: thesis: ( e Joins W .last() ,v,G & not v in W .vertices() implies W .addEdge e is vertex-distinct )

assume that

A1: e Joins W .last() ,v,G and

A2: not v in W .vertices() ; :: thesis: W .addEdge e is vertex-distinct

set W2 = W .addEdge e;

A3: len (W .addEdge e) = (len W) + 2 by A1, Lm37;

for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds

W .addEdge e is vertex-distinct

let W be vertex-distinct Walk of G; :: thesis: for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds

W .addEdge e is vertex-distinct

let e, v be object ; :: thesis: ( e Joins W .last() ,v,G & not v in W .vertices() implies W .addEdge e is vertex-distinct )

assume that

A1: e Joins W .last() ,v,G and

A2: not v in W .vertices() ; :: thesis: W .addEdge e is vertex-distinct

set W2 = W .addEdge e;

A3: len (W .addEdge e) = (len W) + 2 by A1, Lm37;

A4: now :: thesis: for n being odd Element of NAT st n <= len (W .addEdge e) & n > len W holds

( n = len (W .addEdge e) & (W .addEdge e) . n = v )

( n = len (W .addEdge e) & (W .addEdge e) . n = v )

let n be odd Element of NAT ; :: thesis: ( n <= len (W .addEdge e) & n > len W implies ( n = len (W .addEdge e) & (W .addEdge e) . n = v ) )

assume that

A5: n <= len (W .addEdge e) and

A6: n > len W ; :: thesis: ( n = len (W .addEdge e) & (W .addEdge e) . n = v )

(len W) + 1 <= n by A6, NAT_1:13;

then (len W) + 1 < n by XXREAL_0:1;

then ((len W) + 1) + 1 <= n by NAT_1:13;

hence n = len (W .addEdge e) by A3, A5, XXREAL_0:1; :: thesis: (W .addEdge e) . n = v

hence (W .addEdge e) . n = v by A1, A3, Lm38; :: thesis: verum

end;assume that

A5: n <= len (W .addEdge e) and

A6: n > len W ; :: thesis: ( n = len (W .addEdge e) & (W .addEdge e) . n = v )

(len W) + 1 <= n by A6, NAT_1:13;

then (len W) + 1 < n by XXREAL_0:1;

then ((len W) + 1) + 1 <= n by NAT_1:13;

hence n = len (W .addEdge e) by A3, A5, XXREAL_0:1; :: thesis: (W .addEdge e) . n = v

hence (W .addEdge e) . n = v by A1, A3, Lm38; :: thesis: verum

now :: thesis: for m, n being odd Element of NAT st m <= len (W .addEdge e) & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds

m = n

hence
W .addEdge e is vertex-distinct
; :: thesis: verumm = n

let m, n be odd Element of NAT ; :: thesis: ( m <= len (W .addEdge e) & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies m = n )

assume that

A7: m <= len (W .addEdge e) and

A8: n <= len (W .addEdge e) and

A9: (W .addEdge e) . m = (W .addEdge e) . n ; :: thesis: m = n

A10: 1 <= n by ABIAN:12;

A11: 1 <= m by ABIAN:12;

end;assume that

A7: m <= len (W .addEdge e) and

A8: n <= len (W .addEdge e) and

A9: (W .addEdge e) . m = (W .addEdge e) . n ; :: thesis: m = n

A10: 1 <= n by ABIAN:12;

A11: 1 <= m by ABIAN:12;

now :: thesis: m = nend;

hence
m = n
; :: thesis: verumper cases
( m <= len W or m > len W )
;

end;

suppose A12:
m <= len W
; :: thesis: m = n

then
m in dom W
by A11, FINSEQ_3:25;

then A13: (W .addEdge e) . m = W . m by A1, Lm38;

end;then A13: (W .addEdge e) . m = W . m by A1, Lm38;

now :: thesis: m = n

hence
m = n
; :: thesis: verumend;