reconsider p = p as non zero Nat ;
defpred S1[ Element of INT , object ] means $2 = $1 mod p;
A1: for x being Element of INT ex y being Element of Segm p st S1[x,y]
proof
let i be Element of INT ; :: thesis: ex y being Element of Segm p st S1[i,y]
( i mod p >= 0 & i mod p < p ) by NAT_D:62;
then reconsider j = i mod p as Element of NAT by INT_1:3;
A3: j < p by NAT_D:62;
reconsider j = i mod p as Element of Segm p by A3, NAT_1:44;
take j ; :: thesis: S1[i,j]
thus S1[i,j] ; :: thesis: verum
end;
consider f being Function of INT,(Segm p) such that
A4: for x being Element of INT holds S1[x,f . x] from FUNCT_2:sch 3(A1);
 thus ex b1 being Function of INT,(Segm p) st
for x being Element of INT holds b1 . x = x mod p by A4; :: thesis: verum