let G be _Graph; :: thesis:
let W be Walk of G; :: thesis:

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

per cases by A1, XBOOLE_0:def 3;

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

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:

end;

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

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:

end;

end;

end;

hence y in rng W ; :: thesis:

end;

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

let y be object ; :: thesis:
assume y in rng W ; :: thesis:
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;

suppose x is odd ; :: thesis:

then y in W .vertices() by A8, A9, A10, Lm45;
hence y in (W .vertices()) \/ (W .edges()) by XBOOLE_0:def 3; :: thesis:

end;

suppose x is even ; :: thesis:

then y in W .edges() by A8, A9, A11, A10, Lm46;
hence y in (W .vertices()) \/ (W .edges()) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

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

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: