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

assume that

A1: x1 in dom (Special_Function (n1,n2)) and

A2: x2 in dom (Special_Function (n1,n2)) ; :: thesis: ( not (Special_Function (n1,n2)) . x1 = (Special_Function (n1,n2)) . x2 or x1 = x2 )

assume A3: (Special_Function (n1,n2)) . x1 = (Special_Function (n1,n2)) . x2 ; :: thesis: x1 = x2

reconsider x1 = x1 as Element of NAT by A1;

reconsider x2 = x2 as Element of NAT by A2;

A4: ( (Special_Function (n1,n2)) . x2 = IFGT (x2,n1,(x2 + n2),x2) & (Special_Function (n1,n2)) . x1 = IFGT (x1,n1,(x1 + n2),x1) ) by Def2;

assume that

A1: x1 in dom (Special_Function (n1,n2)) and

A2: x2 in dom (Special_Function (n1,n2)) ; :: thesis: ( not (Special_Function (n1,n2)) . x1 = (Special_Function (n1,n2)) . x2 or x1 = x2 )

assume A3: (Special_Function (n1,n2)) . x1 = (Special_Function (n1,n2)) . x2 ; :: thesis: x1 = x2

reconsider x1 = x1 as Element of NAT by A1;

reconsider x2 = x2 as Element of NAT by A2;

A4: ( (Special_Function (n1,n2)) . x2 = IFGT (x2,n1,(x2 + n2),x2) & (Special_Function (n1,n2)) . x1 = IFGT (x1,n1,(x1 + n2),x1) ) by Def2;

per cases
( ( x1 <= n1 & x2 <= n1 ) or ( x1 <= n1 & x2 > n1 ) or ( x2 <= n1 & x1 > n1 ) or ( x1 > n1 & x2 > n1 ) )
;

end;

suppose A5:
( x1 <= n1 & x2 <= n1 )
; :: thesis: x1 = x2

( IFGT (x2,n1,(x2 + n2),x2) = x2 & IFGT (x1,n1,(x1 + n2),x1) = x1 )
by A5, XXREAL_0:def 11;

hence x1 = x2 by A4, A3; :: thesis: verum

end;hence x1 = x2 by A4, A3; :: thesis: verum

suppose A6:
( x1 <= n1 & x2 > n1 )
; :: thesis: x1 = x2

then
IFGT (x2,n1,(x2 + n2),x2) = x2 + n2
by XXREAL_0:def 11;

then A7: (Special_Function (n1,n2)) . x2 = x2 + n2 by Def2;

A8: IFGT (x1,n1,(x1 + n2),x1) = x1 by A6, XXREAL_0:def 11;

A9: (Special_Function (n1,n2)) . x1 = x1 by Def2, A8;

( x1 <> x2 implies (Special_Function (n1,n2)) . x1 <> (Special_Function (n1,n2)) . x2 )

end;then A7: (Special_Function (n1,n2)) . x2 = x2 + n2 by Def2;

A8: IFGT (x1,n1,(x1 + n2),x1) = x1 by A6, XXREAL_0:def 11;

A9: (Special_Function (n1,n2)) . x1 = x1 by Def2, A8;

( x1 <> x2 implies (Special_Function (n1,n2)) . x1 <> (Special_Function (n1,n2)) . x2 )

proof

hence
x1 = x2
by A3; :: thesis: verum
assume
x1 <> x2
; :: thesis: (Special_Function (n1,n2)) . x1 <> (Special_Function (n1,n2)) . x2

( x1 < x2 & 0 <= n2 ) by A6, XXREAL_0:2;

hence (Special_Function (n1,n2)) . x1 <> (Special_Function (n1,n2)) . x2 by A9, A7, XREAL_1:31; :: thesis: verum

end;( x1 < x2 & 0 <= n2 ) by A6, XXREAL_0:2;

hence (Special_Function (n1,n2)) . x1 <> (Special_Function (n1,n2)) . x2 by A9, A7, XREAL_1:31; :: thesis: verum

suppose A10:
( x2 <= n1 & x1 > n1 )
; :: thesis: x1 = x2

A11:
(Special_Function (n1,n2)) . x1 = IFGT (x1,n1,(x1 + n2),x1)
by Def2;

A12: (Special_Function (n1,n2)) . x1 = x1 + n2 by A11, A10, XXREAL_0:def 11;

A13: (Special_Function (n1,n2)) . x2 = IFGT (x2,n1,(x2 + n2),x2) by Def2;

A14: (Special_Function (n1,n2)) . x2 = x2 by A13, A10, XXREAL_0:def 11;

( x2 <> x1 implies (Special_Function (n1,n2)) . x2 <> (Special_Function (n1,n2)) . x1 )

end;A12: (Special_Function (n1,n2)) . x1 = x1 + n2 by A11, A10, XXREAL_0:def 11;

A13: (Special_Function (n1,n2)) . x2 = IFGT (x2,n1,(x2 + n2),x2) by Def2;

A14: (Special_Function (n1,n2)) . x2 = x2 by A13, A10, XXREAL_0:def 11;

( x2 <> x1 implies (Special_Function (n1,n2)) . x2 <> (Special_Function (n1,n2)) . x1 )

proof

hence
x1 = x2
by A3; :: thesis: verum
assume
x2 <> x1
; :: thesis: (Special_Function (n1,n2)) . x2 <> (Special_Function (n1,n2)) . x1

( x2 < x1 & 0 <= n2 ) by A10, XXREAL_0:2;

hence (Special_Function (n1,n2)) . x2 <> (Special_Function (n1,n2)) . x1 by A14, A12, XREAL_1:31; :: thesis: verum

end;( x2 < x1 & 0 <= n2 ) by A10, XXREAL_0:2;

hence (Special_Function (n1,n2)) . x2 <> (Special_Function (n1,n2)) . x1 by A14, A12, XREAL_1:31; :: thesis: verum