let G1, G2 be _Graph; for x being set st G1 == G2 & x is VertexSeq of G1 holds
x is VertexSeq of G2
let x be set ; ( 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
; x is VertexSeq of G2
reconsider x2 = x as FinSequence of the_Vertices_of G2 by A1, A2, GLIB_000:def 34;
now 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),G2let n be
Element of
NAT ;
( 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
;
ex e being set st e Joins x2 . n,x2 . (n + 1),G2consider 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
;
verum end;
hence
x is VertexSeq of G2
by Def1; verum