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