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 5;
hence (W .edgeSeq() ) . n in the_Edges_of G ; :: thesis: verum