let G be _Graph; :: thesis: for W being Walk of G
for n being Element of NAT st n in dom (W .edgeSeq()) holds
(W .edgeSeq()) . n in the_Edges_of G
let W be Walk of G; :: thesis: for n being Element of NAT st n in dom (W .edgeSeq()) holds
(W .edgeSeq()) . n in the_Edges_of G
let n be Element of NAT ; :: thesis: ( n in dom (W .edgeSeq()) implies (W .edgeSeq()) . n in the_Edges_of G )
assume n in dom (W .edgeSeq()) ; :: thesis: (W .edgeSeq()) . n in the_Edges_of G
then (W .edgeSeq()) . n in rng (W .edgeSeq()) by FUNCT_1:def 3;
hence (W .edgeSeq()) . n in the_Edges_of G ; :: thesis: verum