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

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

for W1 being b

( 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