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

A17: now

assume ( i1 = - k & i2 = - l ) ; :: thesis: i1 * i2 is Integer
then i1 * i2 = k * l ;
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 A14, A15, A17; :: thesis: verum