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
rng g = the_Vertices_of G by Def12;
then A2: rng g = the_Vertices_of H by A1;
A3: g is one-to-one by Def12;
g is FinSequence of the_Vertices_of H by A1;
hence g is VertexScheme of H by A3, A2, Def12; :: thesis: verum