let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S
for W being Walk of G ex H being Element of S st W is Walk of H
let G be GraphUnion of S; :: thesis: for W being Walk of G ex H being Element of S st W is Walk of H
defpred S₁[ Walk of G] means ex H being Element of S st $1 is Walk of H;
A1: for W being trivial Walk of G holds S₁[W]

proof

let W be trivial Walk of G; :: thesis: S₁[W]
consider v being Vertex of G such that
A2: W = G .walkOf v by GLIB_001:128;
the_Vertices_of G = union (the_Vertices_of S) by GLIB_014:def 25;
then consider X being set such that
A3: ( v in X & X in the_Vertices_of S ) by TARSKI:def 4;
consider H being _Graph such that
A4: ( H in S & X = the_Vertices_of H ) by A3, GLIB_014:def 14;
reconsider H = H as Element of S by A4;
take H ; :: thesis: W is Walk of H
reconsider w = v as Vertex of H by A3, A4;
W = <*w*> by A2, GLIB_001:def 4
.= H .walkOf w by GLIB_001:def 4 ;
hence W is Walk of H ; :: thesis: verum

end;

A5: for W being Walk of G
for e being object st e in (W .last()) .edgesInOut() & S₁[W] holds
S₁[W .addEdge e]

proof

let W be Walk of G; :: thesis: for e being object st e in (W .last()) .edgesInOut() & S₁[W] holds
S₁[W .addEdge e]
let e be object ; :: thesis: ( e in (W .last()) .edgesInOut() & S₁[W] implies S₁[W .addEdge e] )
assume A6: ( e in (W .last()) .edgesInOut() & S₁[W] ) ; :: thesis: S₁[W .addEdge e]
then consider H being Element of S such that
A7: W is Walk of H ;
reconsider H9 = H as Subgraph of G by GLIB_014:21;
reconsider W9 = W as Walk of H9 by A7;
A8: W .last() = W9 .last() by GLIB_001:16;
e Joins W .last() ,(W .last()) .adj e,G by A6, GLIB_000:67;
then consider H0 being Element of S such that
A9: e Joins W .last() ,(W .last()) .adj e,H0 by GLIBPRE1:117;
W9 .last() in the_Vertices_of H0 by A8, A9, GLIB_000:13;
then the_Vertices_of H meets the_Vertices_of H0 by XBOOLE_0:3;
then e Joins W9 .last() ,(W .last()) .adj e,H9 by A8, A9, Def18;
then e in (W9 .last()) .edgesInOut() by GLIB_000:62;
then W .addEdge e = W9 .addEdge e by GLIB_001:174;
hence S₁[W .addEdge e] ; :: thesis: verum

end;

for W being Walk of G holds S₁[W] from GLIB_009:sch 1(A1, A5);
hence for W being Walk of G ex H being Element of S st W is Walk of H ; :: thesis: verum