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

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