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