let n be Nat; :: thesis: for t, z being Integer st t,z |^ n are_coprime & n > 0 holds
t,z are_coprime
let t, z be Integer; :: thesis: ( t,z |^ n are_coprime & n > 0 implies t,z are_coprime )
assume A1: ( t,z |^ n are_coprime & n > 0 ) ; :: thesis: t,z are_coprime
then A2: ( t divides t |^ n & z divides z |^ n ) by Th6;
( t gcd z divides t & t gcd z divides z ) by INT_2:def 2;
then A3: ( t gcd z divides t |^ n & t gcd z divides z |^ n ) by A2, INT_2:2;
t |^ n,z |^ n are_coprime by A1, WSIERP_1:10;
hence t,z are_coprime by A3, INT_2:13, INT_2:22; :: thesis: verum