for m being Nat st m >= 1 holds
MajP (m,1) = m