set f = delta X;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (delta X) or not x2 in dom (delta X) or not (delta X) . x1 = (delta X) . x2 or x1 = x2 )
assume that
A1: ( x1 in dom (delta X) & x2 in dom (delta X) ) and
A2: (delta X) . x1 = (delta X) . x2 ; :: thesis: x1 = x2
( (delta X) . x1 = [x1,x1] & (delta X) . x2 = [x2,x2] ) by A1, FUNCT_3:def 6;
hence x1 = x2 by A2, XTUPLE_0:1; :: thesis: verum