A . s in Funcs (E,E) ;
hence ^ is Function of E,E by FUNCT_2:66; :: thesis: verum