let F1, F2 be Function of the carrier of USS,(bool (bool the carrier of USS)); :: thesis: ( ( for x being Element of USS holds F1 . x = Neighborhood x ) & ( for x being Element of USS holds F2 . x = Neighborhood x ) implies F1 = F2 )
assume that
A3: for x being Element of USS holds F1 . x = Neighborhood x and
A4: for x being Element of USS holds F2 . x = Neighborhood x ; :: thesis: F1 = F2

now :: thesis: ( dom F1 = dom F2 & ( for x being object st x in dom F1 holds
F1 . x = F2 . x ) )

thus dom F1 = the carrier of USS by FUNCT_2:def 1
.= dom F2 by FUNCT_2:def 1 ; :: thesis: for x being object st x in dom F1 holds
F1 . x = F2 . x

hereby :: thesis: verum

let x be object ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )
assume x in dom F1 ; :: thesis: F1 . x = F2 . x
then reconsider y = x as Element of USS ;
F1 . y = Neighborhood y by A3;
hence F1 . x = F2 . x by A4; :: thesis: verum

end;

end;

hence F1 = F2 by FUNCT_1:def 11; :: thesis: verum