let G1 be _Graph; 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; 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; 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()) <> {}
;
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
;
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;
verum end;