let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2
for W1 being b₁ -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