reconsider n99 = n as Element of NAT by ORDINAL1:def 12;
reconsider m99 = m as Element of NAT by ORDINAL1:def 12;
consider m9 being Nat such that
A1: m = m9 ^2 by Def3;
A2: m9 is odd by A1;
consider n9 being Nat such that
A3: n = n9 ^2 by Def3;
A4: n9 is odd by A3;
A5: (m99 + n99) mod 4 = ((m99 mod 4) + (n99 mod 4)) mod 4 by EULER_2:6
.= (1 + (n99 mod 4)) mod 4 by A1, A2, Th4
.= (1 + 1) mod 4 by A3, A4, Th4
.= 2 by NAT_D:24 ;