let
i
be
Nat
;
:: according to
BASEL_2:def 4
:: thesis:
<%
im1
%>
.
i
is
imaginary
A1
:
i
in
NAT
by
ORDINAL1:def 12
;
(
i
=
0
or
i
>=
1 )
by
NAT_1:14
;
then
(
<%
im1
%>
.
i
=
im1
or
<%
im1
%>
.
i
=
0.
F_Complex
)
by
POLYNOM5:32
,
A1
;
hence
<%
im1
%>
.
i
is
imaginary
;
:: thesis:
verum