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

A5: now

assume that
A6: a <> 0 and
b <> 0 ; :: thesis: a divides b
a |^ e <> 0 by A4, A6, CARD_4:3;
then f = (b |^ e) / (a |^ e) by A3, XCMPLX_1:89
.= (b / a) |^ e by PREPOWER:8 ;
then consider d being Nat such that
A7: f = d |^ e by Th32;
b |^ e = (a * d) |^ e by A3, A7, NEWTON:7;
then b = a * d by A1, Th5;
hence a divides b by NAT_D:def 3; :: thesis: verum

end;

A8: b in REAL by XREAL_0:def 1;

A9: now

assume A10: a = 0 ; :: thesis: a divides b
then 0 divides b |^ e by A1, A2, NAT_1:14, NEWTON:11;
then ex f being Nat st 0 * f = b |^ e by NAT_D:def 3;
hence a divides b by A8, A10, CARD_4:3; :: thesis: verum

end;

now

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

end;

hence a divides b by A9, A5; :: thesis: verum