let m, n be Nat; :: thesis: ( ( ( n mod 4 = 1 & m mod 4 = 1 ) or ( n mod 4 = 3 & m mod 4 = 3 ) ) implies (n * m) mod 4 = 1 )
assume ( ( n mod 4 = 1 & m mod 4 = 1 ) or ( n mod 4 = 3 & m mod 4 = 3 ) ) ; :: thesis: (n * m) mod 4 = 1

per cases then ( ( n mod 4 = 1 & m mod 4 = 1 ) or ( n mod 4 = 3 & m mod 4 = 3 ) ) ;

suppose A1: ( n mod 4 = 1 & m mod 4 = 1 ) ; :: thesis: (n * m) mod 4 = 1

then (n * m) mod 4 = (1 * m) mod 4 by RADIX_2:3;
hence (n * m) mod 4 = 1 by A1; :: thesis: verum

end;

suppose ( n mod 4 = 3 & m mod 4 = 3 ) ; :: thesis: (n * m) mod 4 = 1

then ( (n * m) mod 4 = (3 * m) mod 4 & (3 * m) mod 4 = (3 * 3) mod 4 & 3 * 3 = (4 * 2) + 1 ) by RADIX_2:3;
hence (n * m) mod 4 = 1 by NUMBER02:16; :: thesis: verum

end;

end;