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;