let l, m, n be Nat; :: thesis: (l * m) mod n = (l * (m mod n)) mod n

per cases ( n <> 0 or n = 0 ) ;

suppose n <> 0 ; :: thesis: (l * m) mod n = (l * (m mod n)) mod n

then consider t being Nat such that
A1: m = (n * t) + (m mod n) and
m mod n < n by NAT_D:def 2;
(l * m) mod n = (((l * t) * n) + (l * (m mod n))) mod n by A1;
hence (l * m) mod n = (l * (m mod n)) mod n by NAT_D:21; :: thesis: verum

end;

suppose A2: n = 0 ; :: thesis: (l * m) mod n = (l * (m mod n)) mod n

hence (l * m) mod n = 0 by NAT_D:def 2
.= (l * (m mod n)) mod n by A2, NAT_D:def 2 ;
:: thesis: verum

end;

end;