let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2
for W1 being b₁ -defined Walk of G1
for v, w being object holds
( W1 is_Walk_from v,w iff ( v in dom (F _V) & w in dom (F _V) & F .: W1 is_Walk_from (F _V) . v,(F _V) . w ) )
let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1
for v, w being object holds
( W1 is_Walk_from v,w iff ( v in dom (F _V) & w in dom (F _V) & 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 holds
( W1 is_Walk_from v,w iff ( v in dom (F _V) & w in dom (F _V) & F .: W1 is_Walk_from (F _V) . v,(F _V) . w ) )
let v, w be object ; :: thesis: ( W1 is_Walk_from v,w iff ( v in dom (F _V) & w in dom (F _V) & F .: W1 is_Walk_from (F _V) . v,(F _V) . w ) )
thus ( W1 is_Walk_from v,w implies ( v in dom (F _V) & w in dom (F _V) & F .: W1 is_Walk_from (F _V) . v,(F _V) . w ) ) by Th131, Th132; :: thesis: ( v in dom (F _V) & w in dom (F _V) & F .: W1 is_Walk_from (F _V) . v,(F _V) . w implies W1 is_Walk_from v,w )
assume that
A1: ( v in dom (F _V) & w in dom (F _V) ) and
A2: F .: W1 is_Walk_from (F _V) . v,(F _V) . w ; :: thesis: W1 is_Walk_from v,w
F " (F .: W1) is_Walk_from ((F ") _V) . ((F _V) . v),((F ") _V) . ((F _V) . w) by A2, Th132;
then W1 is_Walk_from ((F _V) ") . ((F _V) . v),((F _V) ") . ((F _V) . w) by Th123;
then W1 is_Walk_from v,((F _V) ") . ((F _V) . w) by A1, FUNCT_1:34;
hence W1 is_Walk_from v,w by A1, FUNCT_1:34; :: thesis: verum