let i, j be natural Number ; ( i * j = 1 implies i = 1 )
assume A1:
i * j = 1
; i = 1
then
i <> 0
;
then consider m being Nat such that
A2:
i = m + 1
by Th6;
j <> 0
by A1;
then consider l being Nat such that
A3:
j = l + 1
by Th6;
A4:
(((m * l) + m) + l) + 1 = 0 + 1
by A1, A2, A3;
then
(m * l) + m = 0
;
hence
i = 1
by A2, A4; verum