let N be Fuzzy_Negation; :: thesis: N in Funcs ([.0,1.],REAL)
N is Function of [.0,1.],REAL by LemmaFunc;
hence N in Funcs ([.0,1.],REAL) by FUNCT_2:8; :: thesis: verum