let e, a, b be Nat; :: thesis: ( e > 0 & a |^ e divides b |^ e implies a divides b )
assume A1: ( e > 0 & a |^ e divides b |^ e ) ; :: thesis: a divides b
then consider f being Nat such that
A2: (a |^ e) * f = b |^ e by NAT_D:def 3;
X: ( a in REAL & b in REAL ) by XREAL_0:def 1;

A4: now

assume A5: a = 0 ; :: thesis: a divides b
then 0 divides b |^ e by A1, NAT_1:14, NEWTON:16;
then ex f being Nat st 0 * f = b |^ e by NAT_D:def 3;
hence a divides b by A5, X, CARD_4:51; :: thesis: verum

end;

A6: now

assume b = 0 ; :: thesis: a divides b
then a * 0 = b ;
hence a divides b by NAT_D:def 3; :: thesis: verum

end;

now

assume ( a <> 0 & b <> 0 ) ; :: thesis: a divides b
then a |^ e <> 0 by X, CARD_4:51;
then f = (b |^ e) / (a |^ e) by A2, XCMPLX_1:90
.= (b / a) |^ e by PREPOWER:15 ;
then consider d being Nat such that
A7: f = d |^ e by Th32;
b |^ e = (a * d) |^ e by A2, A7, NEWTON:12;
then b = a * d by A1, Th5;
hence a divides b by NAT_D:def 3; :: thesis: verum

end;

hence a divides b by A4, A6; :: thesis: verum