let n be natural Number ; :: thesis: for a being Integer holds (a mod n) mod n = a mod n
let a be Integer; :: thesis: (a mod n) mod n = a mod n

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

suppose A1: n = 0 ; :: thesis: (a mod n) mod n = a mod n

hence (a mod n) mod n = 0 by INT_1:def 10
.= a mod n by A1, INT_1:def 10 ;
:: thesis: verum

end;

suppose n <> 0 ; :: thesis: (a mod n) mod n = a mod n

then ( a mod n >= 0 & a mod n < n ) by Th62;
hence (a mod n) mod n = a mod n by Th63; :: thesis: verum

end;

end;