begin
Lm1:
for k being Element of NAT holds
( not k is empty iff 1 <= k )
Lm2:
for f being FinSequence
for n, i being Element of NAT st i <= n holds
(f | (Seg n)) | (Seg i) = f | (Seg i)
Lm3:
Z_3 is finite
by MOD_2:def 20;
begin
begin
begin
Lm4:
unital_poly (F_Complex,1) = <%(- (1_ F_Complex)),(1_ F_Complex)%>
by POLYNOM5:def 4;
begin