let G be _Graph; :: thesis: for W being Walk of G holds rng W = () \/ ()
let W be Walk of G; :: thesis: rng W = () \/ ()
now :: thesis: for y being object st y in () \/ () holds
y in rng W
let y be object ; :: thesis: ( y in () \/ () implies y in rng W )
assume A1: y in () \/ () ; :: thesis: y in rng W
now :: thesis: y in rng W
per cases by ;
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 ;
hence y in rng W by ; :: 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 ;
hence y in rng W by ; :: thesis: verum
end;
end;
end;
hence y in rng W ; :: thesis: verum
end;
then A7: (W .vertices()) \/ () c= rng W by TARSKI:def 3;
now :: thesis: for y being object st y in rng W holds
y in () \/ ()
let y be object ; :: thesis: ( y in rng W implies y in () \/ () )
assume y in rng W ; :: thesis: y in () \/ ()
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 ;
A11: 1 <= x by ;
now :: thesis: y in () \/ ()end;
hence y in () \/ () ; :: thesis: verum
end;
then rng W c= () \/ () by TARSKI:def 3;
hence rng W = () \/ () by ; :: thesis: verum