let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for W1 being b₁ -defined Walk of G1 holds
( W1 .length() = (F .: W1) .length() & len W1 = len (F .: W1) )
let F be non empty PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1 holds
( W1 .length() = (F .: W1) .length() & len W1 = len (F .: W1) )
let W1 be F -defined Walk of G1; :: thesis: ( W1 .length() = (F .: W1) .length() & len W1 = len (F .: W1) )
W1 .edges() = rng (W1 .edgeSeq()) by GLIB_001:def 17;
then A1: rng (W1 .edgeSeq()) c= dom (F _E) by Def35;
then reconsider p = (F _E) * (W1 .edgeSeq()) as FinSequence by FINSEQ_1:16;
thus A2: W1 .length() = len (W1 .edgeSeq()) by GLIB_001:def 18
.= len p by A1, FINSEQ_2:29
.= len ((F .: W1) .edgeSeq()) by Def37
.= (F .: W1) .length() by GLIB_001:def 18 ; :: thesis: len W1 = len (F .: W1)
thus len W1 = (2 * (len (W1 .edgeSeq()))) + 1 by GLIB_001:def 15
.= (2 * (W1 .length())) + 1 by GLIB_001:def 18
.= (2 * (len ((F .: W1) .edgeSeq()))) + 1 by A2, GLIB_001:def 18
.= len (F .: W1) by GLIB_001:def 15 ; :: thesis: verum