let i be Integer; :: thesis: ( i is even implies (i ^2) mod 4 = 0 )
given i9 being Integer such that A1: i = 2 * i9 ; :: according to INT_1:def 3,ABIAN:def 1 :: thesis: (i ^2) mod 4 = 0
i ^2 = (4 * (i9 ^2)) + 0 by A1;
hence (i ^2) mod 4 = 0 mod 4 by EULER_1:12
.= 0 by NAT_D:24 ;
:: thesis: verum