let a, b be Nat; :: thesis: for k, l being Integer st k,l are_relative_prime holds
k |^ a,l |^ b are_relative_prime
let k, l be Integer; :: thesis: ( k,l are_relative_prime implies k |^ a,l |^ b are_relative_prime )
assume k,l are_relative_prime ; :: thesis: k |^ a,l |^ b are_relative_prime
then k |^ a,l are_relative_prime by Th15;
hence k |^ a,l |^ b are_relative_prime by Th15; :: thesis: verum