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 object such that
A1: n in dom (W .edgeSeq()) and
A2: (W .edgeSeq()) . n = e by FUNCT_1:def 3;
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, A2; :: thesis: verum

end;

given n being Element of NAT such that A3: n in dom (W .edgeSeq()) and
A4: (W .edgeSeq()) . n = e ; :: thesis: e in W .edges()
thus e in W .edges() by A3, A4, FUNCT_1:def 3; :: thesis: verum