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)
( rng S = the_Vertices_of G & S is one-to-one ) by Def12;
hence len S = card (the_Vertices_of G) by FINSEQ_4:77; :: thesis: verum