let l, m, n be Integer; :: thesis: (l * m) mod n = (l * (m mod n)) mod n
thus (l * (m mod n)) mod n = ((l mod n) * ((m mod n) mod n)) mod n by NAT_D:67
.= ((l mod n) * (m mod n)) mod n by NAT_D:73
.= (l * m) mod n by NAT_D:67 ; :: thesis: verum