for n being non zero Nat holds card (INT.Group n) = n by Lm1;