theorem Th24: :: BINARI_4:24

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