let G1, G2 be _Graph; :: thesis: for x being set st G1 == G2 & x is VertexSeq of G1 holds
x is VertexSeq of G2
let x be set ; :: thesis: ( G1 == G2 & x is VertexSeq of G1 implies x is VertexSeq of G2 )
assume that
A1: G1 == G2 and
A2: x is VertexSeq of G1 ; :: thesis: x is VertexSeq of G2
reconsider x2 = x as FinSequence of the_Vertices_of G2 by A1, A2, GLIB_000:def 34;

now :: thesis: for n being Element of NAT st 1 <= n & n < len x2 holds
ex e being set st e Joins x2 . n,x2 . (n + 1),G2

let n be Element of NAT ; :: thesis: ( 1 <= n & n < len x2 implies ex e being set st e Joins x2 . n,x2 . (n + 1),G2 )
assume that
A3: 1 <= n and
A4: n < len x2 ; :: thesis: ex e being set st e Joins x2 . n,x2 . (n + 1),G2
consider e being set such that
A5: e Joins x2 . n,x2 . (n + 1),G1 by A2, A3, A4, Def1;
e Joins x2 . n,x2 . (n + 1),G2 by A1, A5, GLIB_000:88;
hence ex e being set st e Joins x2 . n,x2 . (n + 1),G2 ; :: thesis: verum

end;

hence x is VertexSeq of G2 by Def1; :: thesis: verum