let x1, x2 be set ; :: according to FUNCT_1:def 8 :: 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 )
set f = delta X;
assume that
A1: x1 in dom (delta X) and
A2: x2 in dom (delta X) and
A3: (delta X) . x1 = (delta X) . x2 ; :: thesis: x1 = x2
A4: (delta X) . x1 = [x1,x1] by A1, FUNCT_3:def 7;
(delta X) . x2 = [x2,x2] by A2, FUNCT_3:def 7;
hence x1 = x2 by A3, A4, ZFMISC_1:33; :: thesis: verum