let j, m be Nat; :: thesis: ( j <= 2 to_power m implies MajP m,j = m )
assume A1: j <= 2 to_power m ; :: thesis: MajP m,j = m
for k being Nat st 2 to_power k >= j & k >= m holds
k >= m ;
hence MajP m,j = m by A1, Def1; :: thesis: verum