let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2

for W1 being b_{1} -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 ) )

for m, n being odd Element of NAT st m < n & n <= len W1 & W1 . m = W1 . n holds

( m = 1 & n = len W1 )

for W1 being b

( ( 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;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

hereby :: thesis: ( ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )

thus A2:
( F .: W1 is Trail-like implies W1 is Trail-like )
:: thesis: ( 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;(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

proof

assume A4:
F .: W1 is Path-like
; :: thesis: W1 is Path-like
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;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

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

hence
W1 is Path-like
by A2, A4, GLIB_001:def 28; :: thesis: verum
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;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