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

for W1 being b_{1} -defined Walk of G1 holds F " (F .: W1) = W1

let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1 holds F " (F .: W1) = W1

let W1 be F -defined Walk of G1; :: thesis: F " (F .: W1) = W1

W1 .vertices() c= dom (F _V) by Def35;

then A1: rng (W1 .vertexSeq()) c= dom (F _V) by GLIB_001:def 16;

A2: (F " (F .: W1)) .vertexSeq() = ((F ") _V) * ((F .: W1) .vertexSeq()) by Def37

.= ((F _V) ") * ((F _V) * (W1 .vertexSeq())) by Def37

.= (((F _V) ") * (F _V)) * (W1 .vertexSeq()) by RELAT_1:36

.= (id (dom (F _V))) * (W1 .vertexSeq()) by FUNCT_1:39

.= W1 .vertexSeq() by A1, RELAT_1:53 ;

W1 .edges() c= dom (F _E) by Def35;

then A3: rng (W1 .edgeSeq()) c= dom (F _E) by GLIB_001:def 17;

(F " (F .: W1)) .edgeSeq() = ((F ") _E) * ((F .: W1) .edgeSeq()) by Def37

.= ((F _E) ") * ((F _E) * (W1 .edgeSeq())) by Def37

.= (((F _E) ") * (F _E)) * (W1 .edgeSeq()) by RELAT_1:36

.= (id (dom (F _E))) * (W1 .edgeSeq()) by FUNCT_1:39

.= W1 .edgeSeq() by A3, RELAT_1:53 ;

hence F " (F .: W1) = W1 by A2, GLIB_009:26; :: thesis: verum

for W1 being b

let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1 holds F " (F .: W1) = W1

let W1 be F -defined Walk of G1; :: thesis: F " (F .: W1) = W1

W1 .vertices() c= dom (F _V) by Def35;

then A1: rng (W1 .vertexSeq()) c= dom (F _V) by GLIB_001:def 16;

A2: (F " (F .: W1)) .vertexSeq() = ((F ") _V) * ((F .: W1) .vertexSeq()) by Def37

.= ((F _V) ") * ((F _V) * (W1 .vertexSeq())) by Def37

.= (((F _V) ") * (F _V)) * (W1 .vertexSeq()) by RELAT_1:36

.= (id (dom (F _V))) * (W1 .vertexSeq()) by FUNCT_1:39

.= W1 .vertexSeq() by A1, RELAT_1:53 ;

W1 .edges() c= dom (F _E) by Def35;

then A3: rng (W1 .edgeSeq()) c= dom (F _E) by GLIB_001:def 17;

(F " (F .: W1)) .edgeSeq() = ((F ") _E) * ((F .: W1) .edgeSeq()) by Def37

.= ((F _E) ") * ((F _E) * (W1 .edgeSeq())) by Def37

.= (((F _E) ") * (F _E)) * (W1 .edgeSeq()) by RELAT_1:36

.= (id (dom (F _E))) * (W1 .edgeSeq()) by FUNCT_1:39

.= W1 .edgeSeq() by A3, RELAT_1:53 ;

hence F " (F .: W1) = W1 by A2, GLIB_009:26; :: thesis: verum