for j, m being Nat st j <= 2 to_power m holds
MajP (m,j) = m