let G, H be finite _Graph; :: thesis: for g being VertexScheme of G st G == H holds
g is VertexScheme of H
let g be VertexScheme of G; :: thesis: ( G == H implies g is VertexScheme of H )
assume A1: G == H ; :: thesis: g is VertexScheme of H
A2: g is FinSequence of the_Vertices_of H by A1, GLIB_000:def 36;
( g is one-to-one & rng g = the_Vertices_of G ) by Def12;
then ( g is one-to-one & rng g = the_Vertices_of H ) by A1, GLIB_000:def 36;
hence g is VertexScheme of H by A2, Def12; :: thesis: verum