let a, b be Nat; :: thesis: ( a,b are_coprime implies a + b,a * b are_coprime )
assume a,b are_coprime ; :: thesis: a + b,a * b are_coprime
then ( (a + (1 * b)) gcd b = 1 & (b + (1 * a)) gcd a = 1 ) by Th5;
hence a + b,a * b are_coprime by WSIERP_1:7; :: thesis: verum