let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b₁ -valued Walk of G2 holds
( (F _V) * ((F " W2) .vertexSeq()) = W2 .vertexSeq() & (F _E) * ((F " W2) .edgeSeq()) = W2 .edgeSeq() )
let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for W2 being F -valued Walk of G2 holds
( (F _V) * ((F " W2) .vertexSeq()) = W2 .vertexSeq() & (F _E) * ((F " W2) .edgeSeq()) = W2 .edgeSeq() )
let W2 be F -valued Walk of G2; :: thesis: ( (F _V) * ((F " W2) .vertexSeq()) = W2 .vertexSeq() & (F _E) * ((F " W2) .edgeSeq()) = W2 .edgeSeq() )
W2 .vertices() c= rng (F _V) by Def36;
then A1: rng (W2 .vertexSeq()) c= rng (F _V) by GLIB_001:def 16;
(F " W2) .vertexSeq() = ((F _V) ") * (W2 .vertexSeq()) by Def37;
hence (F _V) * ((F " W2) .vertexSeq()) = ((F _V) * ((F _V) ")) * (W2 .vertexSeq()) by RELAT_1:36
.= (id (rng (F _V))) * (W2 .vertexSeq()) by FUNCT_1:39
.= W2 .vertexSeq() by A1, RELAT_1:53 ;
:: thesis: (F _E) * ((F " W2) .edgeSeq()) = W2 .edgeSeq()
W2 .edges() c= rng (F _E) by Def36;
then A2: rng (W2 .edgeSeq()) c= rng (F _E) by GLIB_001:def 17;
(F " W2) .edgeSeq() = ((F _E) ") * (W2 .edgeSeq()) by Def37;
hence (F _E) * ((F " W2) .edgeSeq()) = ((F _E) * ((F _E) ")) * (W2 .edgeSeq()) by RELAT_1:36
.= (id (rng (F _E))) * (W2 .edgeSeq()) by FUNCT_1:39
.= W2 .edgeSeq() by A2, RELAT_1:53 ;
:: thesis: verum