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;
A17: now :: thesis: ( i1 = - k & i2 = - l implies i1 * i2 is Integer )
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 :: thesis: ( ( ( i1 = - k & i2 = l ) or ( i1 = k & i2 = - l ) ) implies i1 * i2 is Integer )
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 Th1; :: thesis: verum
end;
hence i1 * i2 is integer by A16, A15, A17; :: thesis: verum