for c, a, b being Nat st a,b are_coprime holds
for n being non zero Nat holds
( a * b = c |^ n iff ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) ) )