let m, k, n be Nat; :: thesis: ( k <= n implies m |^ k divides m |^ n )
assume k <= n ; :: thesis: m |^ k divides m |^ n
then consider t being Nat such that
A1: n = k + t by NAT_1:10;
reconsider t = t as Element of NAT by ORDINAL1:def 12;
m |^ n = (m |^ k) * (m |^ t) by A1, Th8;
hence m |^ k divides m |^ n by NAT_D:def 3; :: thesis: verum