now :: thesis: for f1, f2 being Function of the carrier of R,INT st ( for a being Element of R holds
( f1 . a = signum (P,a) & ( for a being Element of R holds f2 . a = signum (P,a) ) ) ) holds
f1 = f2

let f1, f2 be Function of the carrier of R,INT; :: thesis: ( ( for a being Element of R holds
( f1 . a = signum (P,a) & ( for a being Element of R holds f2 . a = signum (P,a) ) ) ) implies f1 = f2 )
assume A: for a being Element of R holds
( f1 . a = signum (P,a) & ( for a being Element of R holds f2 . a = signum (P,a) ) ) ; :: thesis: f1 = f2

now :: thesis: for x being object st x in the carrier of R holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in the carrier of R implies f1 . x = f2 . x )
assume x in the carrier of R ; :: thesis: f1 . x = f2 . x
then reconsider a = x as Element of R ;
thus f1 . x = signum (P,a) by A
.= f2 . x by A ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum

end;

hence for b₁, b₂ being Function of the carrier of R,INT st ( for a being Element of R holds b₁ . a = signum (P,a) ) & ( for a being Element of R holds b₂ . a = signum (P,a) ) holds
b₁ = b₂ ; :: thesis: verum