let f, g be Function of INT,(Segm p); :: thesis: ( ( for x being Element of INT holds f . x = x mod p ) & ( for x being Element of INT holds g . x = x mod p ) implies f = g )
assume that
A5: for x being Element of INT holds f . x = x mod p and
A6: for x being Element of INT holds g . x = x mod p ; :: thesis: f = g

now :: thesis: for x being Element of INT holds f . x = g . x

let x be Element of INT ; :: thesis: f . x = g . x
f . x = x mod p by A5;
hence f . x = g . x by A6; :: thesis: verum

end;

hence f = g ; :: thesis: verum