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

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