let N be Fuzzy_Negation; :: thesis: N is Function of [.0,1.],REAL
rng N c= REAL by RELAT_1:def 19;
hence N is Function of [.0,1.],REAL by FUNCT_2:6; :: thesis: verum