consider l being Element of NAT such that
A15: ( i2 = l or i2 = - l ) by Th8;
consider k being Element of NAT such that
A16: ( i1 = k or i1 = - k ) by Th8;

A17: now

assume that
A18: i1 = - k and
A19: i2 = - l ; :: thesis: i1 * i2 is Integer
i1 * i2 = k * l by A18, A19;
hence i1 * i2 is Integer ; :: thesis: verum

end;

now

assume ( ( i1 = - k & i2 = l ) or ( i1 = k & i2 = - l ) ) ; :: thesis: i1 * i2 is Integer
then i1 * i2 = - (k * l) ;
hence i1 * i2 is Integer by Th7; :: thesis: verum

end;

hence i1 * i2 is integer by A16, A15, A17; :: thesis: verum