let k, j, i be Nat; :: thesis: ( k ^2 < j & i mod j = k implies (i ^2 ) mod j = k ^2 )
assume A1: ( k ^2 < j & i mod j = k ) ; :: thesis: (i ^2 ) mod j = k ^2
then consider n being Nat such that
A2: ( i = (j * n) + k & k < j ) by NAT_D:def 2;
i ^2 = (j * ((((n * j) * n) + (k * n)) + (n * k))) + (k ^2 ) by A2;
then (i ^2 ) mod j = (k ^2 ) mod j by NAT_D:21;
hence (i ^2 ) mod j = k ^2 by A1, NAT_D:24; :: thesis: verum