reconsider p = p as non zero Nat ;
defpred S₁[ Element of INT , object ] means $2 = $1 mod p;
A1: for x being Element of INT ex y being Element of Segm p st S₁[x,y]

proof

let i be Element of INT ; :: thesis: ex y being Element of Segm p st S₁[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: S₁[i,j]
thus S₁[i,j] ; :: thesis: verum

end;

consider f being Function of INT,(Segm p) such that
A4: for x being Element of INT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
thus ex b₁ being Function of INT,(Segm p) st
for x being Element of INT holds b₁ . x = x mod p by A4; :: thesis: verum