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

assume that

A16: x1 in dom (Special_Function4 (n1,n2)) and

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

assume A18: (Special_Function4 (n1,n2)) . x1 = (Special_Function4 (n1,n2)) . x2 ; :: thesis: x1 = x2

reconsider x1 = x1 as Element of NAT by A16;

reconsider x2 = x2 as Element of NAT by A17;

assume that

A16: x1 in dom (Special_Function4 (n1,n2)) and

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

assume A18: (Special_Function4 (n1,n2)) . x1 = (Special_Function4 (n1,n2)) . x2 ; :: thesis: x1 = x2

reconsider x1 = x1 as Element of NAT by A16;

reconsider x2 = x2 as Element of NAT by A17;

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

end;

suppose A19:
( x1 <= n1 + 1 & x2 <= n1 + 1 )
; :: thesis: x1 = x2

A20:
( (Special_Function4 (n1,n2)) . x2 = IFGT (x2,(n1 + 1),(x2 + n2),x2) & (Special_Function4 (n1,n2)) . x1 = IFGT (x1,(n1 + 1),(x1 + n2),x1) )
by Def5;

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

hence x1 = x2 by A20, A18; :: thesis: verum

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

hence x1 = x2 by A20, A18; :: thesis: verum

suppose A21:
( x1 > n1 + 1 & x2 <= n1 + 1 )
; :: thesis: x1 = x2

A22:
( (Special_Function4 (n1,n2)) . x2 = IFGT (x2,(n1 + 1),(x2 + n2),x2) & (Special_Function4 (n1,n2)) . x1 = IFGT (x1,(n1 + 1),(x1 + n2),x1) )
by Def5;

A23: ( (Special_Function4 (n1,n2)) . x2 = x2 & (Special_Function4 (n1,n2)) . x1 = x1 + n2 ) by A22, A21, XXREAL_0:def 11;

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

end;A23: ( (Special_Function4 (n1,n2)) . x2 = x2 & (Special_Function4 (n1,n2)) . x1 = x1 + n2 ) by A22, A21, XXREAL_0:def 11;

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

proof

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

( (Special_Function4 (n1,n2)) . x1 > (n1 + 1) + n2 & (n1 + 1) + n2 >= n1 + 1 ) by A23, A21, XREAL_1:6, XREAL_1:31;

hence (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 by A21, A23, XXREAL_0:2; :: thesis: verum

end;( (Special_Function4 (n1,n2)) . x1 > (n1 + 1) + n2 & (n1 + 1) + n2 >= n1 + 1 ) by A23, A21, XREAL_1:6, XREAL_1:31;

hence (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 by A21, A23, XXREAL_0:2; :: thesis: verum

suppose A24:
( x1 <= n1 + 1 & x2 > n1 + 1 )
; :: thesis: x1 = x2

A25:
( (Special_Function4 (n1,n2)) . x2 = IFGT (x2,(n1 + 1),(x2 + n2),x2) & (Special_Function4 (n1,n2)) . x1 = IFGT (x1,(n1 + 1),(x1 + n2),x1) & IFGT (x2,(n1 + 1),(x2 + n2),x2) = x2 + n2 & IFGT (x1,(n1 + 1),(x1 + n2),x1) = x1 )
by Def5, A24, XXREAL_0:def 11;

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

end;( x1 <> x2 implies (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 )

proof

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

( (Special_Function4 (n1,n2)) . x2 > (n1 + 1) + n2 & (n1 + 1) + n2 >= n1 + 1 ) by A25, A24, XREAL_1:6, XREAL_1:31;

hence (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 by A24, A25, XXREAL_0:2; :: thesis: verum

end;( (Special_Function4 (n1,n2)) . x2 > (n1 + 1) + n2 & (n1 + 1) + n2 >= n1 + 1 ) by A25, A24, XREAL_1:6, XREAL_1:31;

hence (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 by A24, A25, XXREAL_0:2; :: thesis: verum

suppose A26:
( x1 > n1 + 1 & x2 > n1 + 1 )
; :: thesis: x1 = x2

A27:
( (Special_Function4 (n1,n2)) . x2 = IFGT (x2,(n1 + 1),(x2 + n2),x2) & (Special_Function4 (n1,n2)) . x1 = IFGT (x1,(n1 + 1),(x1 + n2),x1) )
by Def5;

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

then x1 + n2 = x2 + n2 by A27, A18;

hence x1 = x2 ; :: thesis: verum

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

then x1 + n2 = x2 + n2 by A27, A18;

hence x1 = x2 ; :: thesis: verum