let G1, G2 be _Graph; :: thesis: for x being set st G1 == G2 & x is Walk of G1 holds

x is Walk of G2

let x be set ; :: thesis: ( G1 == G2 & x is Walk of G1 implies x is Walk of G2 )

assume that

A1: G1 == G2 and

A2: x is Walk of G1 ; :: thesis: x is Walk of G2

A3: the_Vertices_of G1 = the_Vertices_of G2 by A1, GLIB_000:def 34;

then reconsider W = x as FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) by A1, A2, GLIB_000:def 34;

hence x is Walk of G2 by A2, A4, Def3; :: thesis: verum

x is Walk of G2

let x be set ; :: thesis: ( G1 == G2 & x is Walk of G1 implies x is Walk of G2 )

assume that

A1: G1 == G2 and

A2: x is Walk of G1 ; :: thesis: x is Walk of G2

A3: the_Vertices_of G1 = the_Vertices_of G2 by A1, GLIB_000:def 34;

then reconsider W = x as FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) by A1, A2, GLIB_000:def 34;

A4: now :: thesis: for n being odd Element of NAT st n < len W holds

W . (n + 1) Joins W . n,W . (n + 2),G2

W . 1 in the_Vertices_of G2
by A2, A3, Def3;W . (n + 1) Joins W . n,W . (n + 2),G2

let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G2 )

assume n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G2

then W . (n + 1) Joins W . n,W . (n + 2),G1 by A2, Def3;

hence W . (n + 1) Joins W . n,W . (n + 2),G2 by A1, GLIB_000:88; :: thesis: verum

end;assume n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G2

then W . (n + 1) Joins W . n,W . (n + 2),G1 by A2, Def3;

hence W . (n + 1) Joins W . n,W . (n + 2),G2 by A1, GLIB_000:88; :: thesis: verum

hence x is Walk of G2 by A2, A4, Def3; :: thesis: verum