let G be _Graph; :: thesis: for W being Walk of G holds rng W = (W .vertices()) \/ (W .edges())

let W be Walk of G; :: thesis: rng W = (W .vertices()) \/ (W .edges())

hence rng W = (W .vertices()) \/ (W .edges()) by A7, XBOOLE_0:def 10; :: thesis: verum

let W be Walk of G; :: thesis: rng W = (W .vertices()) \/ (W .edges())

now :: thesis: for y being object st y in (W .vertices()) \/ (W .edges()) holds

y in rng W

then A7:
(W .vertices()) \/ (W .edges()) c= rng W
by TARSKI:def 3;y in rng W

let y be object ; :: thesis: ( y in (W .vertices()) \/ (W .edges()) implies y in rng W )

assume A1: y in (W .vertices()) \/ (W .edges()) ; :: thesis: y in rng W

end;assume A1: y in (W .vertices()) \/ (W .edges()) ; :: thesis: y in rng W

now :: thesis: y in rng Wend;

hence
y in rng W
; :: thesis: verumper cases
( y in W .vertices() or y in W .edges() )
by A1, XBOOLE_0:def 3;

end;

now :: thesis: for y being object st y in rng W holds

y in (W .vertices()) \/ (W .edges())

then
rng W c= (W .vertices()) \/ (W .edges())
by TARSKI:def 3;y in (W .vertices()) \/ (W .edges())

let y be object ; :: thesis: ( y in rng W implies y in (W .vertices()) \/ (W .edges()) )

assume y in rng W ; :: thesis: y in (W .vertices()) \/ (W .edges())

then consider x being Nat such that

A8: x in dom W and

A9: W . x = y by FINSEQ_2:10;

A10: x <= len W by A8, FINSEQ_3:25;

A11: 1 <= x by A8, FINSEQ_3:25;

end;assume y in rng W ; :: thesis: y in (W .vertices()) \/ (W .edges())

then consider x being Nat such that

A8: x in dom W and

A9: W . x = y by FINSEQ_2:10;

A10: x <= len W by A8, FINSEQ_3:25;

A11: 1 <= x by A8, FINSEQ_3:25;

now :: thesis: y in (W .vertices()) \/ (W .edges())end;

hence
y in (W .vertices()) \/ (W .edges())
; :: thesis: verumper cases
( x is odd or x is even )
;

end;

suppose
x is odd
; :: thesis: y in (W .vertices()) \/ (W .edges())

then
y in W .vertices()
by A8, A9, A10, Lm45;

hence y in (W .vertices()) \/ (W .edges()) by XBOOLE_0:def 3; :: thesis: verum

end;hence y in (W .vertices()) \/ (W .edges()) by XBOOLE_0:def 3; :: thesis: verum

suppose
x is even
; :: thesis: y in (W .vertices()) \/ (W .edges())

then
y in W .edges()
by A8, A9, A11, A10, Lm46;

hence y in (W .vertices()) \/ (W .edges()) by XBOOLE_0:def 3; :: thesis: verum

end;hence y in (W .vertices()) \/ (W .edges()) by XBOOLE_0:def 3; :: thesis: verum

hence rng W = (W .vertices()) \/ (W .edges()) by A7, XBOOLE_0:def 10; :: thesis: verum