let G be _Graph; :: thesis: for W being Walk of G
for e being set holds
( e in W .edges() iff ex n being Element of NAT st
( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e ) )
let W be Walk of G; :: thesis: for e being set holds
( e in W .edges() iff ex n being Element of NAT st
( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e ) )
let e be set ; :: thesis: ( e in W .edges() iff ex n being Element of NAT st
( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e ) )

hereby :: thesis: ( ex n being Element of NAT st
( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e ) implies e in W .edges() )

assume e in W .edges() ; :: thesis: ex n being Element of NAT st
( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e )
then consider n being set such that
A1: ( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A1;
take n = n; :: thesis: ( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e )
thus ( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e ) by A1; :: thesis: verum

end;

given n being Element of NAT such that A2: ( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e ) ; :: thesis: e in W .edges()
thus e in W .edges() by A2, FUNCT_1:def 5; :: thesis: verum