( dom (delta X) = X & rng (delta X) c= [:X,X:] ) by Def6, Th47;
hence delta X is Function of X,[:X,X:] by FUNCT_2:2; :: thesis: verum