let k, l be odd square Integer; :: thesis: (k + l) mod 8 = 2
( 1 |^ 2 is square & (2 * 0) + 1 is odd & 1 is integer ) ;
then A1: ( (k - 1) mod 8 = 0 & (l - 1) mod 8 = 0 ) by N0319;
(k + l) mod 8 = ((k - 1) + ((l - 1) + 2)) mod 8
.= (((k - 1) mod 8) + (((l - 1) + 2) mod 8)) mod 8 by NAT_D:66
.= (((l - 1) mod 8) + (2 mod 8)) mod 8 by NAT_D:66, A1
.= 2 mod (2 + 6) by A1
.= 2 ;
hence (k + l) mod 8 = 2 ; :: thesis: verum