let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (Special_Function2 n) or not x2 in dom (Special_Function2 n) or not (Special_Function2 n) . x1 = (Special_Function2 n) . x2 or x1 = x2 )

assume that

A1: x1 in dom (Special_Function2 n) and

A2: x2 in dom (Special_Function2 n) ; :: thesis: ( not (Special_Function2 n) . x1 = (Special_Function2 n) . x2 or x1 = x2 )

assume A3: (Special_Function2 n) . x1 = (Special_Function2 n) . x2 ; :: thesis: x1 = x2

reconsider x1 = x1 as Element of NAT by A1;

reconsider x2 = x2 as Element of NAT by A2;

(Special_Function2 n) . x2 = x2 + n by Def3;

then x1 + n = x2 + n by A3, Def3;

hence x1 = x2 ; :: thesis: verum

assume that

A1: x1 in dom (Special_Function2 n) and

A2: x2 in dom (Special_Function2 n) ; :: thesis: ( not (Special_Function2 n) . x1 = (Special_Function2 n) . x2 or x1 = x2 )

assume A3: (Special_Function2 n) . x1 = (Special_Function2 n) . x2 ; :: thesis: x1 = x2

reconsider x1 = x1 as Element of NAT by A1;

reconsider x2 = x2 as Element of NAT by A2;

(Special_Function2 n) . x2 = x2 + n by Def3;

then x1 + n = x2 + n by A3, Def3;

hence x1 = x2 ; :: thesis: verum