begin
theorem Th1:
theorem Th2:
theorem Th3:
Lm1:
for x, y being Real st ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) holds
y <= 0
theorem Th4:
theorem Th5:
theorem Th6:
theorem
canceled;
theorem Th8:
:: deftheorem Def1 defines |. POLYNOM5:def 1 :
theorem Th9:
theorem Th10:
theorem
theorem
theorem Th13:
theorem
theorem Th15:
begin
:: deftheorem defines `^ POLYNOM5:def 2 :
theorem Th16:
theorem
theorem
theorem
theorem Th20:
theorem Th21:
theorem
theorem Th23:
Lm2:
for L being non empty ZeroStr
for p being AlgSequence of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
theorem Th24:
:: deftheorem Def3 defines * POLYNOM5:def 3 :
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem defines <% POLYNOM5:def 4 :
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem Th45:
theorem
theorem
theorem Th48:
theorem
begin
:: deftheorem Def5 defines Subst POLYNOM5:def 5 :
theorem Th50:
theorem
theorem
theorem Th53:
theorem Th54:
begin
:: deftheorem Def6 defines is_a_root_of POLYNOM5:def 6 :
:: deftheorem Def7 defines with_roots POLYNOM5:def 7 :
theorem Th55:
theorem
:: deftheorem Def8 defines algebraic-closed POLYNOM5:def 8 :
:: deftheorem Def9 defines Roots POLYNOM5:def 9 :
:: deftheorem Def10 defines NormPolynomial POLYNOM5:def 10 :
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem
theorem Th63:
theorem Th64:
:: deftheorem Def11 defines FPower POLYNOM5:def 11 :
theorem
theorem
theorem Th67:
theorem
theorem
theorem Th70:
theorem Th71:
:: deftheorem Def12 defines Polynomial-Function POLYNOM5:def 12 :
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75: