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