let a, b, c be Nat; :: thesis: ( a divides b implies a |^ c divides b |^ c )
assume a divides b ; :: thesis: a |^ c divides b |^ c
then consider d being Nat such that
A1: a * d = b by NAT_D:def 3;
b |^ c = (a |^ c) * (d |^ c) by A1, NEWTON:7;
hence a |^ c divides b |^ c ; :: thesis: verum