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

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

for W1 being b

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