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

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

for W2 being b

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