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