let n be Nat; :: thesis: ( (4 * n) mod 8 = 0 or (4 * n) mod 8 = 4 )
A1: not not n mod (7 + 1) = 0 & ... & not n mod (7 + 1) = 7 by NUMBER03:11;
A2: ( ((1 * 8) + 0) mod 8 = 0 & ((1 * 8) + 4) mod 8 = 4 & ((2 * 8) + 0) mod 8 = 0 & ((2 * 8) + 4) mod 8 = 4 & ((3 * 8) + 0) mod 8 = 0 & ((3 * 8) + 4) mod 8 = 4 ) by NAT_D:def 2;
4 mod 8 = 4 by NAT_D:24;
then not not (4 * n) mod (7 + 1) = (4 * 0) mod 8 & ... & not (4 * n) mod (7 + 1) = (4 * 7) mod 8 by A1, NAT_D:67;
hence ( (4 * n) mod 8 = 0 or (4 * n) mod 8 = 4 ) by A2; :: thesis: verum