f +* (x,e) is Function of VAR,E ;
hence x / (e,) is Function of VAR,E ; :: thesis: verum