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
( v in dom (F _V) & w in dom (F _V) )
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
( v in dom (F _V) & w in dom (F _V) )
let W1 be F -defined Walk of G1; :: thesis: for v, w being object st W1 is_Walk_from v,w holds
( v in dom (F _V) & w in dom (F _V) )
let v, w be object ; :: thesis: ( W1 is_Walk_from v,w implies ( v in dom (F _V) & w in dom (F _V) ) )
assume W1 is_Walk_from v,w ; :: thesis: ( v in dom (F _V) & w in dom (F _V) )
then ( W1 .first() = v & W1 .last() = w ) by GLIB_001:def 23;
then ( v in W1 .vertices() & w in W1 .vertices() ) by GLIB_001:88;
hence ( v in dom (F _V) & w in dom (F _V) ) by Def35, TARSKI:def 3; :: thesis: verum