let x1, x2 be object ; FUNCT_1:def 4 ( 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))
; ( 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
; 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 ) )
;
suppose A19:
(
x1 <= n1 + 1 &
x2 <= n1 + 1 )
;
x1 = x2A20:
(
(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;
verum end; suppose A21:
(
x1 > n1 + 1 &
x2 <= n1 + 1 )
;
x1 = x2
(
(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;
then A23:
(
(Special_Function4 (n1,n2)) . x2 = x2 &
(Special_Function4 (n1,n2)) . x1 = x1 + n2 )
by A21, XXREAL_0:def 11;
(
x1 <> x2 implies
(Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 )
proof
assume
x1 <> x2
;
(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;
verum
end; hence
x1 = x2
by A18;
verum end; suppose A24:
(
x1 <= n1 + 1 &
x2 > n1 + 1 )
;
x1 = x2then 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, XXREAL_0:def 11;
(
x1 <> x2 implies
(Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 )
proof
assume
x1 <> x2
;
(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;
verum
end; hence
x1 = x2
by A18;
verum end; suppose A26:
(
x1 > n1 + 1 &
x2 > n1 + 1 )
;
x1 = x2A27:
(
(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
;
verum end; end;