let t, u, z be Integer; :: thesis: ( (t + (u * z)) gcd z = t gcd z & (t - (u * z)) gcd z = t gcd z )
(t - (u * z)) gcd z = t gcd z
proof
(t - (u * z)) gcd z = ((t - (u * z)) + (u * z)) gcd z by Lm0d
.= t gcd z ;
hence (t - (u * z)) gcd z = t gcd z ; :: thesis: verum
end;
hence ( (t + (u * z)) gcd z = t gcd z & (t - (u * z)) gcd z = t gcd z ) by Lm0d; :: thesis: verum