let G1, G2 be _Graph; :: thesis: for G being GraphUnion of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 holds
for W being Walk of G holds
( W is Walk of G1 or W is Walk of G2 )
let G be GraphUnion of G1,G2; :: thesis: ( G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 implies for W being Walk of G holds
( W is Walk of G1 or W is Walk of G2 ) )
assume A1: ( G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 ) ; :: thesis: for W being Walk of G holds
( W is Walk of G1 or W is Walk of G2 )
then A2: G is Supergraph of G2 by GLIB_014:26;
then A3: ( G1 is Subgraph of G & G2 is Subgraph of G ) by GLIB_006:57;
A4: the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) by A1, GLIB_014:25;
A5: the_Edges_of G = (the_Edges_of G1) \/ (the_Edges_of G2) by A1, GLIB_014:25;
defpred S₁[ Walk of G] means ( $1 is Walk of G1 or $1 is Walk of G2 );
A6: 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
A7: W = G .walkOf v by GLIB_001:128;

per cases ( v in the_Vertices_of G1 or v in the_Vertices_of G2 ) by A4, XBOOLE_0:def 3;

suppose v in the_Vertices_of G1 ; :: thesis: S₁[W]

then W .first() in the_Vertices_of G1 by A7;
hence S₁[W] by A3, GLIB_001:168; :: thesis: verum

end;

suppose v in the_Vertices_of G2 ; :: thesis: S₁[W]

then W .first() in the_Vertices_of G2 by A7;
hence S₁[W] by A3, GLIB_001:168; :: thesis: verum

end;

end;

end;

A8: 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 e in (W .last()) .edgesInOut() ; :: thesis: ( not S₁[W] or S₁[W .addEdge e] )
then consider w being Vertex of G such that
A9: e Joins W .last() ,w,G by GLIB_000:64;
assume S₁[W] ; :: thesis: S₁[W .addEdge e]

per cases then ( W is Walk of G1 or W is Walk of G2 ) ;

suppose W is Walk of G1 ; :: thesis: S₁[W .addEdge e]

then reconsider W1 = W as Walk of G1 ;
e in the_Edges_of G1

proof

assume A10: not e in the_Edges_of G1 ; :: thesis: contradiction
e in the_Edges_of G by A9, GLIB_000:def 13;
then e in the_Edges_of G2 by A5, A10, XBOOLE_0:def 3;
then e Joins W .last() ,w,G2 by A2, A9, GLIB_006:72;
then W .last() in the_Vertices_of G2 by GLIB_000:13;
then W1 .last() in the_Vertices_of G2 ;
hence contradiction by A1, XBOOLE_0:3; :: thesis: verum

end;

then e Joins W .last() ,w,G1 by A9, GLIB_006:72;
then e Joins W1 .last() ,w,G1 ;
then e in (W1 .last()) .edgesInOut() by GLIB_000:62;
then W1 .addEdge e = W .addEdge e by A3, GLIB_001:174;
hence S₁[W .addEdge e] ; :: thesis: verum

end;

suppose W is Walk of G2 ; :: thesis: S₁[W .addEdge e]

then reconsider W2 = W as Walk of G2 ;
e in the_Edges_of G2

proof

assume A11: not e in the_Edges_of G2 ; :: thesis: contradiction
e in the_Edges_of G by A9, GLIB_000:def 13;
then e in the_Edges_of G1 by A5, A11, XBOOLE_0:def 3;
then e Joins W .last() ,w,G1 by A9, GLIB_006:72;
then W .last() in the_Vertices_of G1 by GLIB_000:13;
then W2 .last() in the_Vertices_of G1 ;
hence contradiction by A1, XBOOLE_0:3; :: thesis: verum

end;

then e Joins W .last() ,w,G2 by A2, A9, GLIB_006:72;
then e Joins W2 .last() ,w,G2 ;
then e in (W2 .last()) .edgesInOut() by GLIB_000:62;
then W2 .addEdge e = W .addEdge e by A3, GLIB_001:174;
hence S₁[W .addEdge e] ; :: thesis: verum

end;

end;

end;

for W being Walk of G holds S₁[W] from GLIB_009:sch 1(A6, A8);
hence for W being Walk of G holds
( W is Walk of G1 or W is Walk of G2 ) ; :: thesis: verum