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;