let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
let G2 be Subgraph of G1; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
let W2 be Walk of G2; :: thesis: ( W1 = W2 implies ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) ) )
assume A1: W1 = W2 ; :: thesis: ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
then A2: W1 .last() = W2 .last() ;
W1 .first() = W2 .first() by A1;
hence ( W1 is closed iff W2 is closed ) by A2; :: thesis: ( ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
now :: thesis: ( ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed Walk of G1 ) )
hereby :: thesis: ( W2 is directed implies W1 is directed Walk of G1 )
assume A3: W1 is directed ; :: thesis: W2 is directed
now :: thesis: for n being odd Element of NAT st n < len W2 holds
(the_Source_of G2) . (W2 . (n + 1)) = W2 . n
let n be odd Element of NAT ; :: thesis: ( n < len W2 implies (the_Source_of G2) . (W2 . (n + 1)) = W2 . n )
A4: 1 <= n + 1 by NAT_1:12;
assume A5: n < len W2 ; :: thesis: (the_Source_of G2) . (W2 . (n + 1)) = W2 . n
then n + 1 <= len W2 by NAT_1:13;
then n + 1 in dom W2 by A4, FINSEQ_3:25;
then W2 . (n + 1) in the_Edges_of G2 by Th7;
then (the_Source_of G2) . (W2 . (n + 1)) = (the_Source_of G1) . (W2 . (n + 1)) by GLIB_000:def 32;
hence (the_Source_of G2) . (W2 . (n + 1)) = W2 . n by A1, A3, A5; :: thesis: verum
end;
hence W2 is directed ; :: thesis: verum
end;
assume W2 is directed ; :: thesis: W1 is directed Walk of G1
hence W1 is directed Walk of G1 by A1, Th173; :: thesis: verum
end;
hence ( W1 is directed iff W2 is directed ) ; :: thesis: ( ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
( W1 is V5() iff len W2 = 1 ) by A1, Lm55;
hence ( W1 is V5() iff W2 is V5() ) by Lm55; :: thesis: ( ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
( W1 is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W2 holds
W2 . m <> W2 . n ) by A1, Lm57;
hence A6: ( W1 is Trail-like iff W2 is Trail-like ) by Lm57; :: thesis: ( ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
( W1 is Path-like iff ( W1 is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len W2 & W2 . m = W2 . n holds
( m = 1 & n = len W2 ) ) ) ) by A1;
hence ( W1 is Path-like iff W2 is Path-like ) by A6; :: thesis: ( W1 is vertex-distinct iff W2 is vertex-distinct )
( W1 is vertex-distinct iff for m, n being odd Element of NAT st m <= len W2 & n <= len W2 & W2 . m = W2 . n holds
m = n ) by A1;
hence ( W1 is vertex-distinct iff W2 is vertex-distinct ) ; :: thesis: verum