let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for W1 being b₁ -defined Walk of G1 holds (F .: W1) .vertices() = (F _V) .: (W1 .vertices())
let F be non empty PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1 holds (F .: W1) .vertices() = (F _V) .: (W1 .vertices())
let W1 be F -defined Walk of G1; :: thesis: (F .: W1) .vertices() = (F _V) .: (W1 .vertices())
A1: (F .: W1) .vertices() = rng ((F .: W1) .vertexSeq()) by GLIB_001:def 16
.= rng ((F _V) * (W1 .vertexSeq())) by Def37 ;
for y being object holds
( y in rng ((F _V) * (W1 .vertexSeq())) iff y in (F _V) .: (W1 .vertices()) )

proof

let y be object ; :: thesis: ( y in rng ((F _V) * (W1 .vertexSeq())) iff y in (F _V) .: (W1 .vertices()) )

hereby :: thesis: ( y in (F _V) .: (W1 .vertices()) implies y in rng ((F _V) * (W1 .vertexSeq())) )

assume y in rng ((F _V) * (W1 .vertexSeq())) ; :: thesis: y in (F _V) .: (W1 .vertices())
then consider x being object such that
A2: ( x in dom ((F _V) * (W1 .vertexSeq())) & ((F _V) * (W1 .vertexSeq())) . x = y ) by FUNCT_1:def 3;
set v = (W1 .vertexSeq()) . x;
x in dom (W1 .vertexSeq()) by A2, FUNCT_1:11;
then (W1 .vertexSeq()) . x in rng (W1 .vertexSeq()) by FUNCT_1:3;
then A3: (W1 .vertexSeq()) . x in W1 .vertices() by GLIB_001:def 16;
A4: (W1 .vertexSeq()) . x in dom (F _V) by A2, FUNCT_1:11;
(F _V) . ((W1 .vertexSeq()) . x) = y by A2, FUNCT_1:12;
hence y in (F _V) .: (W1 .vertices()) by A3, A4, FUNCT_1:def 6; :: thesis: verum

end;

assume y in (F _V) .: (W1 .vertices()) ; :: thesis: y in rng ((F _V) * (W1 .vertexSeq()))
then consider v being object such that
A5: ( v in dom (F _V) & v in W1 .vertices() & (F _V) . v = y ) by FUNCT_1:def 6;
v in rng (W1 .vertexSeq()) by A5, GLIB_001:def 16;
then consider x being object such that
A6: ( x in dom (W1 .vertexSeq()) & (W1 .vertexSeq()) . x = v ) by FUNCT_1:def 3;
A7: ((F _V) * (W1 .vertexSeq())) . x = y by A5, A6, FUNCT_1:13;
x in dom ((F _V) * (W1 .vertexSeq())) by A5, A6, FUNCT_1:11;
hence y in rng ((F _V) * (W1 .vertexSeq())) by A7, FUNCT_1:3; :: thesis: verum

end;

hence (F .: W1) .vertices() = (F _V) .: (W1 .vertices()) by A1, TARSKI:2; :: thesis: verum