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 .: (F " W2) = W2
let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for W2 being F -valued Walk of G2 holds F .: (F " W2) = W2
let W2 be F -valued Walk of G2; :: thesis: F .: (F " W2) = W2
W2 .vertices() c= rng (F _V) by Def36;
then A1: rng (W2 .vertexSeq()) c= rng (F _V) by GLIB_001:def 16;
A2: (F .: (F " W2)) .vertexSeq() = (F _V) * (((F ") .: W2) .vertexSeq()) by Def37
.= (F _V) * (((F ") _V) * (W2 .vertexSeq())) by Def37
.= ((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 ;
W2 .edges() c= rng (F _E) by Def36;
then A3: rng (W2 .edgeSeq()) c= rng (F _E) by GLIB_001:def 17;
(F .: (F " W2)) .edgeSeq() = (F _E) * (((F ") .: W2) .edgeSeq()) by Def37
.= (F _E) * (((F ") _E) * (W2 .edgeSeq())) by Def37
.= ((F _E) * ((F _E) ")) * (W2 .edgeSeq()) by RELAT_1:36
.= (id (rng (F _E))) * (W2 .edgeSeq()) by FUNCT_1:39
.= W2 .edgeSeq() by A3, RELAT_1:53 ;
hence F .: (F " W2) = W2 by A2, GLIB_009:26; :: thesis: verum