consider l being Nat such that
A15:
( i2 = l or i2 = - l )
by Th2;
consider k being Nat such that
A16:
( i1 = k or i1 = - k )
by Th2;
now ( ( ( i1 = - k & i2 = l ) or ( i1 = k & i2 = - l ) ) implies i1 * i2 is Integer )end;
hence
i1 * i2 is integer
by A16, A15, A17; verum