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