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

now :: thesis: for y being object st y in (W .vertices()) \/ (W .edges()) holds
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

now :: thesis: y in rng W

per cases ( y in W .vertices() or y in W .edges() ) by A1, XBOOLE_0:def 3;

suppose y in W .vertices() ; :: thesis: y in rng W

then consider x being odd Element of NAT such that
A2: x <= len W and
A3: W . x = y by Lm45;
1 <= x by ABIAN:12;
then x in dom W by A2, FINSEQ_3:25;
hence y in rng W by A3, FUNCT_1:def 3; :: thesis: verum

end;

suppose y in W .edges() ; :: thesis: y in rng W

then consider x being even Element of NAT such that
A4: 1 <= x and
A5: x <= len W and
A6: W . x = y by Lm46;
x in dom W by A4, A5, FINSEQ_3:25;
hence y in rng W by A6, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence y in rng W ; :: thesis: verum

end;

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

now :: thesis: for y being object st y in rng W holds
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;

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

per cases ( x is odd or x is even ) ;

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;

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;

end;

end;

hence y in (W .vertices()) \/ (W .edges()) ; :: thesis: verum

end;

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