let a, b be Nat; :: thesis: for c, d being non zero Nat st a mod (c * d) = b mod (c * d) holds
a mod c = b mod c
let c, d be non zero Nat; :: thesis: ( a mod (c * d) = b mod (c * d) implies a mod c = b mod c )
assume a mod (c * d) = b mod (c * d) ; :: thesis: a mod c = b mod c
then (a mod (c * d)) mod c = b mod c by RADIX_1:3;
hence a mod c = b mod c by RADIX_1:3; :: thesis: verum