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

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