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;

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 ) )

hence
x is EdgeSeq of G2
by Def2; :: thesis: verum( 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;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