let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for W1 being b₁ -defined Walk of G1
for v, w being object st W1 is_Walk_from v,w holds
F .: W1 is_Walk_from (F _V) . v,(F _V) . w
let F be non empty PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1
for v, w being object st W1 is_Walk_from v,w holds
F .: W1 is_Walk_from (F _V) . v,(F _V) . w
let W1 be F -defined Walk of G1; :: thesis: for v, w being object st W1 is_Walk_from v,w holds
F .: W1 is_Walk_from (F _V) . v,(F _V) . w
let v, w be object ; :: thesis: ( W1 is_Walk_from v,w implies F .: W1 is_Walk_from (F _V) . v,(F _V) . w )
assume W1 is_Walk_from v,w ; :: thesis: F .: W1 is_Walk_from (F _V) . v,(F _V) . w
then ( W1 .first() = v & W1 .last() = w ) by GLIB_001:def 23;
then ( W1 . 1 = v & W1 . (len W1) = w ) by GLIB_001:def 6, GLIB_001:def 7;
then ( (F _V) . v = (F .: W1) . 1 & (F _V) . w = (F .: W1) . (len W1) ) by Th129, ABIAN:12, POLYFORM:4;
then ( (F _V) . v = (F .: W1) .first() & (F _V) . w = (F .: W1) . (len (F .: W1)) ) by GLIB_001:def 6, Th125;
then ( (F _V) . v = (F .: W1) .first() & (F _V) . w = (F .: W1) .last() ) by GLIB_001:def 7;
hence F .: W1 is_Walk_from (F _V) . v,(F _V) . w by GLIB_001:def 23; :: thesis: verum