for M being finite Cardinal ex n being Nat st M = card n