let G1, G2 be _Graph; for F being non empty PGraphMapping of G1,G2
for W1 being b1 -defined Walk of G1 holds
( (F _V) . (W1 .first()) = (F .: W1) .first() & (F _V) . (W1 .last()) = (F .: W1) .last() )
let F be non empty PGraphMapping of G1,G2; for W1 being F -defined Walk of G1 holds
( (F _V) . (W1 .first()) = (F .: W1) .first() & (F _V) . (W1 .last()) = (F .: W1) .last() )
let W1 be F -defined Walk of G1; ( (F _V) . (W1 .first()) = (F .: W1) .first() & (F _V) . (W1 .last()) = (F .: W1) .last() )
set n = len (W1 .vertexSeq());
1 <= len (W1 .vertexSeq())
by GLIB_001:67;
then A1:
( 1 in dom (W1 .vertexSeq()) & len (W1 .vertexSeq()) in dom (W1 .vertexSeq()) )
by FINSEQ_3:25;
W1 .vertices() = rng (W1 .vertexSeq())
by GLIB_001:def 16;
then A2:
rng (W1 .vertexSeq()) c= dom (F _V)
by Def35;
then reconsider p = (F _V) * (W1 .vertexSeq()) as FinSequence by FINSEQ_1:16;
A3: len (W1 .vertexSeq()) =
len p
by A2, FINSEQ_2:29
.=
len ((F .: W1) .vertexSeq())
by Def37
;
thus (F _V) . (W1 .first()) =
(F _V) . ((W1 .vertexSeq()) . 1)
by GLIB_001:71
.=
((F _V) * (W1 .vertexSeq())) . 1
by A1, FUNCT_1:13
.=
((F .: W1) .vertexSeq()) . 1
by Def37
.=
(F .: W1) .first()
by GLIB_001:71
; (F _V) . (W1 .last()) = (F .: W1) .last()
thus (F _V) . (W1 .last()) =
(F _V) . ((W1 .vertexSeq()) . (len (W1 .vertexSeq())))
by GLIB_001:71
.=
((F _V) * (W1 .vertexSeq())) . (len (W1 .vertexSeq()))
by A1, FUNCT_1:13
.=
((F .: W1) .vertexSeq()) . (len (W1 .vertexSeq()))
by Def37
.=
(F .: W1) .last()
by A3, GLIB_001:71
; verum