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

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