per cases ( a <> 0 or a = 0 ) ;

suppose a <> 0 ; :: thesis: a ** X is finite

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

end;

suppose A1: a = 0 ; :: thesis: a ** X is finite

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: a ** X is finite

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

end;

suppose not X is empty ; :: thesis: a ** X is finite

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

end;

end;

end;

end;