let a, b, c, d, n be Nat; :: thesis: ( a,b,c are_mutually_coprime & (a * b) * c = d |^ n implies ex k being Nat st a = k |^ n )
assume A1: a,b,c are_mutually_coprime ; :: thesis: ( not (a * b) * c = d |^ n or ex k being Nat st a = k |^ n )
assume (a * b) * c = d |^ n ; :: thesis: ex k being Nat st a = k |^ n
then ex k1 being Nat st k1 |^ n = a * b by A1, NEWTON02:30, INT_2:26;
hence ex k being Nat st a = k |^ n by A1, NEWTON02:30; :: thesis: verum