per cases ;

suppose a <> 0 ; :: thesis:

hence a ** X is finite by Th3, CARD_1:38; :: thesis:

end;

suppose A1: a = 0 ; :: thesis:

per cases ;

suppose X is empty ; :: thesis:

hence a ** X is finite by INTEGRA2:7; :: thesis:

end;

suppose not X is empty ; :: thesis:

hence a ** X is finite by A1, Th4; :: thesis:

end;

end;

end;

end;