let G be _finite _Graph; :: thesis: for S being VertexScheme of G holds len S = card (the_Vertices_of G)
let S be VertexScheme of G; :: thesis: len S = card (the_Vertices_of G)
A1: S is one-to-one by Def12;
rng S = the_Vertices_of G by Def12;
hence len S = card (the_Vertices_of G) by A1, FINSEQ_4:62; :: thesis: verum