let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for W1 being b1 -defined Walk of G1 holds
( ( W1 is V5() implies F .: W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )
let F be non empty PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1 holds
( ( W1 is V5() implies F .: W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )
let W1 be F -defined Walk of G1; :: thesis: ( ( W1 is V5() implies F .: W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )
hereby :: thesis: ( ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )
assume W1 is V5() ; :: thesis: F .: W1 is V5()
then W1 .length() = 0 by GLIB_001:def 26;
then (F .: W1) .length() = 0 by Th125;
hence F .: W1 is V5() by GLIB_001:def 26; :: thesis: verum
end;
hereby :: thesis: ( ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )
assume A1: W1 is closed ; :: thesis: F .: W1 is closed
(F .: W1) .first() = (F _V) . (W1 .first()) by Th127
.= (F _V) . (W1 .last()) by A1, GLIB_001:def 24
.= (F .: W1) .last() by Th127 ;
hence F .: W1 is closed by GLIB_001:def 24; :: thesis: verum
end;
thus A2: ( F .: W1 is Trail-like implies W1 is Trail-like ) :: thesis: ( F .: W1 is Path-like implies W1 is Path-like )
proof
assume F .: W1 is Trail-like ; :: thesis: W1 is Trail-like
then (F .: W1) .edgeSeq() is one-to-one by GLIB_001:def 27;
then A3: (F _E) * (W1 .edgeSeq()) is one-to-one by Def37;
W1 .edges() = rng (W1 .edgeSeq()) by GLIB_001:def 17;
then rng (W1 .edgeSeq()) c= dom (F _E) by Def35;
then W1 .edgeSeq() is one-to-one by A3, FUNCT_1:25;
hence W1 is Trail-like by GLIB_001:def 27; :: thesis: verum
end;
assume A4: F .: W1 is Path-like ; :: thesis: W1 is Path-like
for m, n being odd Element of NAT st m < n & n <= len W1 & W1 . m = W1 . n holds
( m = 1 & n = len W1 )
proof
let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len W1 & W1 . m = W1 . n implies ( m = 1 & n = len W1 ) )
assume A5: ( m < n & n <= len W1 ) ; :: thesis: ( not W1 . m = W1 . n or ( m = 1 & n = len W1 ) )
A6: len W1 = (2 * (len (W1 .edgeSeq()))) + 1 by GLIB_001:def 15
.= (2 * (W1 .length())) + 1 by GLIB_001:def 18
.= (2 * ((F .: W1) .length())) + 1 by Th125
.= (2 * (len ((F .: W1) .edgeSeq()))) + 1 by GLIB_001:def 18
.= len (F .: W1) by GLIB_001:def 15 ;
assume A7: W1 . n = W1 . m ; :: thesis: ( m = 1 & n = len W1 )
(F .: W1) . n = (F _V) . (W1 . n) by A5, Th129
.= (F .: W1) . m by A5, A7, Th129, XXREAL_0:2 ;
then ( m = 1 & n = len (F .: W1) ) by A4, A5, A6, GLIB_001:def 28;
hence ( m = 1 & n = len W1 ) by A6; :: thesis: verum
end;
hence W1 is Path-like by A2, A4, GLIB_001:def 28; :: thesis: verum