let G1 be _Graph; :: thesis: for G2 being removeLoops of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
let G2 be removeLoops of G1; :: thesis: for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
let W1 be Walk of G1; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
A1: W1 is_Walk_from W1 .first() ,W1 .last() by GLIB_001:def 23;
set P = the Path of W1;
set v = W1 .first() ;
set w = W1 .last() ;
A2: the Path of W1 is_Walk_from W1 .first() ,W1 .last() by A1, GLIB_001:160;

per cases ( ( the Path of W1 .edges()) /\ (G1 .loops()) = {} or ( the Path of W1 .edges()) /\ (G1 .loops()) <> {} ) ;

suppose ( the Path of W1 .edges()) /\ (G1 .loops()) = {} ; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

then the Path of W1 .edges() c= (the_Edges_of G1) \ (G1 .loops()) by XBOOLE_0:def 7, XBOOLE_1:86;
then A3: the Path of W1 .edges() c= the_Edges_of G2 by GLIB_000:53;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:53;
then the Path of W1 .vertices() c= the_Vertices_of G2 ;
then reconsider W2 = the Path of W1 as Walk of G2 by A3, GLIB_001:170;
take W2 ; :: thesis: W2 is_Walk_from W1 .first() ,W1 .last()
thus W2 is_Walk_from W1 .first() ,W1 .last() by A2, GLIB_001:19; :: thesis: verum

end;

suppose ( the Path of W1 .edges()) /\ (G1 .loops()) <> {} ; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

then consider v0, e being object such that
A4: ( e Joins v0,v0,G1 & the Path of W1 = G1 .walkOf (v0,e,v0) ) by Th57, XBOOLE_0:def 7;
( the Path of W1 .first() = v0 & the Path of W1 .last() = v0 ) by A4, GLIB_001:15;
then A5: ( v0 = W1 .first() & v0 = W1 .last() ) by A2, GLIB_001:def 23;
v0 in the_Vertices_of G1 by A4, GLIB_000:13;
then reconsider v0 = v0 as Vertex of G2 by GLIB_000:53;
take G2 .walkOf v0 ; :: thesis: G2 .walkOf v0 is_Walk_from W1 .first() ,W1 .last()
thus G2 .walkOf v0 is_Walk_from W1 .first() ,W1 .last() by A5, GLIB_001:13; :: thesis: verum

end;

end;