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