let G1, G2 be _Graph; :: thesis: for x being set st G1 == G2 & x is EdgeSeq of G1 holds
x is EdgeSeq of G2
let x be set ; :: thesis: ( G1 == G2 & x is EdgeSeq of G1 implies x is EdgeSeq of G2 )
assume that
A1: G1 == G2 and
A2: x is EdgeSeq of G1 ; :: thesis: x is EdgeSeq of G2
reconsider es = x as EdgeSeq of G1 by A2;
reconsider es2 = es as FinSequence of the_Edges_of G2 by A1, GLIB_000:def 34;
consider vs being FinSequence of the_Vertices_of G1 such that
A3: len vs = (len es) + 1 and
A4: for n being Element of NAT st 1 <= n & n <= len es holds
es . n Joins vs . n,vs . (n + 1),G1 by Def2;

now :: thesis: ex vs being FinSequence of the_Vertices_of G2 st
( len vs = (len es) + 1 & ( for n being Element of NAT st 1 <= n & n <= len es2 holds
es2 . n Joins vs . n,vs . (n + 1),G2 ) )

reconsider vs = vs as FinSequence of the_Vertices_of G2 by A1, GLIB_000:def 34;
take vs = vs; :: thesis: ( len vs = (len es) + 1 & ( for n being Element of NAT st 1 <= n & n <= len es2 holds
es2 . n Joins vs . n,vs . (n + 1),G2 ) )
thus len vs = (len es) + 1 by A3; :: thesis: for n being Element of NAT st 1 <= n & n <= len es2 holds
es2 . n Joins vs . n,vs . (n + 1),G2
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len es2 implies es2 . n Joins vs . n,vs . (n + 1),G2 )
assume that
A5: 1 <= n and
A6: n <= len es2 ; :: thesis: es2 . n Joins vs . n,vs . (n + 1),G2
es2 . n Joins vs . n,vs . (n + 1),G1 by A4, A5, A6;
hence es2 . n Joins vs . n,vs . (n + 1),G2 by A1, GLIB_000:88; :: thesis: verum

end;

hence x is EdgeSeq of G2 by Def2; :: thesis: verum