let N, M be ExtNat; :: thesis: ( N * M = 1 implies N = 1 )
assume A1: N * M = 1 ; :: thesis: N = 1
( N <> +infty & M <> +infty )

proof

assume ( N = +infty or M = +infty ) ; :: thesis: contradiction
then ( ( N = +infty & ( M is zero or M is positive ) ) or ( M = +infty & ( N is zero or N is positive ) ) ) ;
hence contradiction by A1, XXREAL_3:def 5; :: thesis: verum

end;

then reconsider n = N, m = M as Nat by Th3;
n * m = 1 by A1;
hence N = 1 by NAT_1:15; :: thesis: verum