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 ) ) 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
.= (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 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 ())) + 1 by GLIB_001:def 15
.= (2 * ()) + 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
.= (F .: W1) . m by ;
then ( m = 1 & n = len (F .: W1) ) by ;
hence ( m = 1 & n = len W1 ) by A6; :: thesis: verum
end;
hence W1 is Path-like by ; :: thesis: verum