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 ) )

A4: (W .edgeSeq()) . n = e ; :: thesis: e in W .edges()

thus e in W .edges() by A3, A4, FUNCT_1:def 3; :: thesis: verum

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() )

given n being Element of NAT such that A3:
n in dom (W .edgeSeq())
and ( 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;( 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

A4: (W .edgeSeq()) . n = e ; :: thesis: e in W .edges()

thus e in W .edges() by A3, A4, FUNCT_1:def 3; :: thesis: verum