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