( ( [:X,X:] = {} implies X = {} ) & dom (delta X) = X & rng (delta X) c= [:X,X:] ) by Def7, Th66;
hence delta X is Function of X,[:X,X:] by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum