A1: ( [: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 A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum