let a, b, c be Nat; :: thesis: ( (a mod c) * (b mod c) = c implies (a * b) mod c = 0 )
assume (a mod c) * (b mod c) = c ; :: thesis: (a * b) mod c = 0
then c mod c = ((a mod c) * (b mod c)) mod c ;
hence (a * b) mod c = 0 by NAT_D:67; :: thesis: verum