let G be _Graph; :: thesis: for W being Walk of G
for v being Vertex of G st v in W .vertices() holds
G .walkOf v is_substring_of W, 0
let W be Walk of G; :: thesis: for v being Vertex of G st v in W .vertices() holds
G .walkOf v is_substring_of W, 0
let v be Vertex of G; :: thesis: ( v in W .vertices() implies G .walkOf v is_substring_of W, 0 )
assume v in W .vertices() ; :: thesis: G .walkOf v is_substring_of W, 0
then consider n being odd Element of NAT such that
A1: ( n <= len W & W . n = v ) by GLIB_001:87;

now :: thesis: ( len (G .walkOf v) > 0 implies ex n being odd Element of NAT st
( 0 <= n & n <= len W & mid (W,n,((n -' 1) + (len (G .walkOf v)))) = G .walkOf v ) )

assume len (G .walkOf v) > 0 ; :: thesis: ex n being odd Element of NAT st
( 0 <= n & n <= len W & mid (W,n,((n -' 1) + (len (G .walkOf v)))) = G .walkOf v )
take n = n; :: thesis: ( 0 <= n & n <= len W & mid (W,n,((n -' 1) + (len (G .walkOf v)))) = G .walkOf v )
thus 0 <= n ; :: thesis: ( n <= len W & mid (W,n,((n -' 1) + (len (G .walkOf v)))) = G .walkOf v )
thus n <= len W by A1; :: thesis: mid (W,n,((n -' 1) + (len (G .walkOf v)))) = G .walkOf v
A3: (n -' 1) + (len (G .walkOf v)) = (n -' 1) + 1 by GLIB_001:13
.= (n + 1) -' 1 by ABIAN:12, NAT_D:38
.= (n + 1) - 1 by NAT_D:37
.= n ;
1 <= n by ABIAN:12;
then A4: n in dom W by A1, FINSEQ_3:25;
thus mid (W,n,((n -' 1) + (len (G .walkOf v)))) = <*(W . n)*> by A3, A4, Th7
.= G .walkOf v by A1, GLIB_001:def 4 ; :: thesis: verum

end;

hence G .walkOf v is_substring_of W, 0 by FINSEQ_8:def 7; :: thesis: verum