let i, j, k be Nat; :: thesis: ( k ^2 < j & i mod j = k implies (i ^2) mod j = k ^2 )
assume that
A1: k ^2 < j and
A2: i mod j = k ; :: thesis: (i ^2) mod j = k ^2
consider n being Nat such that
A3: i = (j * n) + k and
k < j by A1, A2, NAT_D:def 2;
i ^2 = (j * ((((n * j) * n) + (k * n)) + (n * k))) + (k ^2) by A3;
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