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;

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

hence
x is VertexSeq of G2
by Def1; :: thesis: verumex 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;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