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;
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 ) ; :: 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 ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
( x1 <> x2 implies (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 )
proof
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 ;
hence (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 by ; :: thesis: verum
end;
hence x1 = x2 by A18; :: thesis: verum
end;
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 ;
( x1 <> x2 implies (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 )
proof
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 ;
hence (Special_Function4 (n1,n2)) . x2 <> (Special_Function4 (n1,n2)) . x1 by ; :: thesis: verum
end;
hence x1 = x2 by A18; :: thesis: verum
end;
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 ;
then x1 + n2 = x2 + n2 by ;
hence x1 = x2 ; :: thesis: verum
end;
end;