let X be set ; :: thesis: rng (delta X) c= [:X,X:]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (delta X) or y in [:X,X:] )
assume y in rng (delta X) ; :: thesis: y in [:X,X:]
then consider x being object such that
A1: x in dom (delta X) and
A2: y = (delta X) . x by FUNCT_1:def 3;
A3: x in X by A1, Def6;
then y = [x,x] by A2, Def6;
hence y in [:X,X:] by A3, ZFMISC_1:87; :: thesis: verum