let m, n be Nat; :: thesis: m gcd (m * n) = m
A1: m divides m * n ;
for d being Nat st d divides m & d divides m * n holds
d divides m ;
hence m gcd (m * n) = m by A1, NAT_D:def 5; :: thesis: verum