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 () & () . 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 () & () . n = e ) )

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

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

then consider n being object such that
A1: n in dom () 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 () & () . n = e )
thus ( n in dom () & () . n = e ) by A1, A2; :: thesis: verum
end;
given n being Element of NAT such that A3: n in dom () and
A4: (W .edgeSeq()) . n = e ; :: thesis:
thus e in W .edges() by ; :: thesis: verum