let i, j be natural Number ; :: thesis: ( i * j = 1 implies i = 1 )
assume A1: i * j = 1 ; :: thesis: 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; :: thesis: verum