let W1 be F -defined Walk of G1; :: thesis: ( W1 = F " W2 iff ( (F _V) * (W1 .vertexSeq()) = W2 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = W2 .edgeSeq() ) )
thus ( W1 = F " W2 implies ( (F _V) * (W1 .vertexSeq()) = W2 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = W2 .edgeSeq() ) ) by Lm5; :: thesis: ( (F _V) * (W1 .vertexSeq()) = W2 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = W2 .edgeSeq() implies W1 = F " W2 )
assume that
A1: (F _V) * (W1 .vertexSeq()) = W2 .vertexSeq() and
A2: (F _E) * (W1 .edgeSeq()) = W2 .edgeSeq() ; :: thesis: W1 = F " W2
( rng (W1 .vertexSeq()) = W1 .vertices() & rng (W1 .edgeSeq()) = W1 .edges() ) by GLIB_001:def 16, GLIB_001:def 17;
then A3: ( rng (W1 .vertexSeq()) c= dom (F _V) & rng (W1 .edgeSeq()) c= dom (F _E) ) by Def35;
A4: ((F ") _V) * (W2 .vertexSeq()) = (((F _V) ") * (F _V)) * (W1 .vertexSeq()) by A1, RELAT_1:36
.= (id (dom (F _V))) * (W1 .vertexSeq()) by FUNCT_1:39
.= W1 .vertexSeq() by A3, RELAT_1:53 ;
((F ") _E) * (W2 .edgeSeq()) = (((F _E) ") * (F _E)) * (W1 .edgeSeq()) by A2, RELAT_1:36
.= (id (dom (F _E))) * (W1 .edgeSeq()) by FUNCT_1:39
.= W1 .edgeSeq() by A3, RELAT_1:53 ;
hence W1 = F " W2 by A4, Def37; :: thesis: verum