The Mizar article:

Little Bezout Theorem (Factor Theorem)

by
Piotr Rudnicki

Received December 30, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: UPROOTS
[ MML identifier index ]


environ

 vocabulary ARYTM_1, SQUARE_1, ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, RLVECT_1,
      BOOLE, FINSEQ_2, FINSEQ_4, BINOP_1, VECTSP_1, LATTICES, NORMSP_1,
      COMPLFLD, GROUP_1, REALSET1, POLYNOM1, TARSKI, CARD_1, CARD_3, SETWISEO,
      ALGSEQ_1, POLYNOM3, POLYNOM2, ALGSTR_2, FUNCT_4, VECTSP_2, FUNCOP_1,
      FUNCT_2, SEQM_3, RFINSEQ, POLYNOM5, FVSUM_1, FINSET_1, NEWTON, MCART_1,
      SGRAPH1, CAT_1, DTCONSTR, PBOOLE, MEMBERED, ANPROJ_1, UPROOTS;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, NUMBERS, XREAL_0, ZFMISC_1,
      REAL_1, NAT_1, SETWISEO, RLVECT_1, VECTSP_1, VECTSP_2, BINOP_1, RELAT_1,
      FUNCT_1, FUNCT_2, SETWOP_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSOP_1,
      TOPREAL1, NORMSP_1, BINARITH, RVSUM_1, ALGSEQ_1, COMPLFLD, POLYNOM3,
      POLYNOM4, POLYNOM5, CARD_1, FINSET_1, GROUP_1, MCART_1, PRE_CIRC,
      FUNCT_4, RLVECT_2, CQC_LANG, DTCONSTR, RFINSEQ, POLYNOM1, FVSUM_1,
      WSIERP_1, PBOOLE, SEQM_3, MEMBERED, REALSET1;
 constructors REAL_1, FINSOP_1, MONOID_0, WELLORD2, TOPREAL1, BINARITH,
      POLYNOM4, FVSUM_1, POLYNOM5, PREPOWER, SETWOP_2, WELLFND1, PRE_CIRC,
      FINSEQOP, ALGSTR_1, RLVECT_2, CQC_LANG, POLYNOM2, WSIERP_1, SETWISEO,
      GOBOARD1;
 clusters XREAL_0, STRUCT_0, RELSET_1, SEQ_1, VECTSP_1, VECTSP_2, FINSEQ_2,
      POLYNOM1, POLYNOM3, MONOID_0, NAT_1, INT_1, POLYNOM5, FINSEQ_1, FINSET_1,
      CARD_1, MEMBERED, FUNCT_1, ALGSTR_1, SUBSET_1, ORDINAL2, RFINSEQ,
      GOBRD13, PRE_CIRC, PRELAMB, CHAIN_1, POLYNOM7;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions TARSKI, VECTSP_2, FUNCT_1, POLYNOM5;
 theorems GROUP_1, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2,
      RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, REAL_1, XCMPLX_1,
      POLYNOM5, BINARITH, INT_1, XCMPLX_0, SCMFSA_7, AXIOMS, RVSUM_1, FVSUM_1,
      FINSEQ_3, FINSEQ_2, FINSEQ_4, POLYNOM4, POLYNOM3, NORMSP_1, FUNCT_7,
      ALGSEQ_1, RLVECT_1, FINSET_1, PBOOLE, FUNCOP_1, POLYNOM1, MATRIX_3,
      PRE_CIRC, VECTSP_2, CARD_2, FINSEQ_5, GRAPH_5, QC_LANG4, CQC_LANG,
      DTCONSTR, BAGORDER, RFINSEQ, GOBOARD9, WELLORD2, CARD_3, ORDINAL2, FSM_1,
      JORDAN3, FINSOP_1, MONOID_0, INTEGRA1, SEQM_3, TRIANG_1, FUNCT_4,
      MCART_1, REALSET1;
 schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FRAENKEL, POLYNOM2, INT_2,
      ALGSEQ_1, RECDEF_1;

begin :: Preliminaries

theorem neNat1: :: neNat1:
for n being Nat holds n is non empty iff n = 1 or n > 1
proof let n be Nat;
 hereby assume n is non empty; then n <> 0; then 0 < n by NAT_1:19; then
   0+1 <= n by NAT_1:38;
  hence n = 1 or n > 1 by REAL_1:def 5;
 end;
 assume n = 1 or n > 1; then n <> 0;
 hence thesis;
end;

theorem SumFS: :: SumFS:
for f being FinSequence of NAT
 st for i being Nat st i in dom f holds f.i <> 0
  holds Sum f = len f iff f = (len f) |-> 1
proof let f be FinSequence of NAT;
 defpred P[Nat] means 
  for f being FinSequence of NAT
   st len f = $1 &
      for i being Nat st i in dom f holds f.i <> 0
    holds Sum f = len f iff f = (len f) |-> 1;
BA: P[0] proof let f be FinSequence of NAT such that
    A: len f = 0 and for i being Nat st i in dom f holds f.i <> 0;
       f = {} by A, FINSEQ_1:25; then
    B: f = <*>REAL;
       hereby assume Sum f = len f;
        thus f = {} by A, FINSEQ_1:25 .= (len f) |-> 1 by A, FINSEQ_2:72;
       end;
       assume f = (len f) |-> 1;
       thus Sum f = len f by A, B, RVSUM_1:102;
    end;
IS: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume
    A: P[n];
     let f be FinSequence of NAT such that
    B: len f = n+1 and
    D: for i being Nat st i in dom f holds f.i <> 0;
       len f <> 0 by B;
       then consider g being FinSequence of NAT, a being Nat such that
    E: f = g^<*a*> by FINSEQ_2:22;
    Ea: g is FinSequence of REAL by FINSEQ_2:27;
       n+1 = len g + len <*a*> by B, E, FINSEQ_1:35; then
       n+1 = len g + 1 by FINSEQ_1:57; then       
    F: len g = n by XCMPLX_1:2;
    G: now let i be Nat; assume
       A1: i in dom g;
           dom g c= dom f by E, FINSEQ_1:39; then
       B1: i in dom f by A1;
           f.i = g.i by A1, E, FINSEQ_1:def 7;
         hence g.i <> 0 by B1, D;
       end;
    I: Sum f = Sum g + a by E, Ea, RVSUM_1:104;
    J: len f in Seg len f by B, FINSEQ_1:6;
    K: dom f = Seg len f by FINSEQ_1:def 3;
       f.len f = a by E, F, B, FINSEQ_1:59; then
       a <> 0 by J, K, D; then 0 < a by NAT_1:19; then
    L: 0+1 <= a by NAT_1:38;
     hereby assume A1: Sum f = len f;
         reconsider h = (len g) |-> (1 qua Real) as FinSequence of REAL;
     X1: len h = len g by FINSEQ_2:69;
     Z1: h is Element of (len h)-tuples_on REAL by FINSEQ_2:110;
     Y1: g is Element of (len g)-tuples_on REAL by Ea, FINSEQ_2:110;     
         now let j be Nat; assume
         A2: j in Seg len g; then
             j in dom g by FINSEQ_1:def 3; then
             g.j <> 0 by G; then 0 < g.j by NAT_1:19;
             then 0+1 <= g.j by NAT_1:38;
          hence h.j <= g.j by A2, FINSEQ_2:70;
         end; then
     E1: Sum h <= Sum g by Z1, Y1, X1, RVSUM_1:112;
     F1: Sum h = n*1 by F, RVSUM_1:110 .= n;
     G1: Sum g = Sum g +a -a by XCMPLX_1:26 .= n+1 -a by B, I, A1; then
         n <= n+1-a by E1, F1; then
         n+a <= n+1-a+a by AXIOMS:24; then
         n+a <= n+1 by XCMPLX_1:27; then
         a <= 1 by REAL_1:53; then
     D1: a = 1 by L, AXIOMS:21; then
         Sum g = len g by F, G1, XCMPLX_1:26; then
         g = (len g) |-> 1 by F, G, A;
      hence f = (len f) |-> 1 by D1, B, E, F, FINSEQ_2:74;
     end;
     assume f = (len f) |-> 1; then
         f = (n |-> 1)^(1 |-> 1) by B, FINSEQ_2:143
          .= (n |-> 1)^<*1*> by FINSEQ_2:73; then
     A1: g = (len g) |-> 1 & a = 1 by E, F, FINSEQ_2:20; 
     B1: Sum g = len g by F, G, A1, A;
     thus Sum f = len f by A1, I, B, B1, F;
    end;
 for n being Nat holds P[n] from Ind(BA, IS);
 hence thesis;
end;

:: Stolen from POLYNOM2
scheme IndFinSeq0 { F() -> FinSequence, P[set, set]} :
for i being Nat st 1 <= i & i <= len F() holds P[i, F().i]
provided
 A1: P[1, F().1] and
 A2: for i being Nat st 1 <= i & i < len F()
      holds P[i, F().i] implies P[i+1, F().(i+1)]
proof
defpred Q[Nat] means 1 <= $1 & $1 <= len F() & not(P[$1, F().($1)]);
assume not(for i being Nat st 1 <= i & i <= len F() holds P[i, F().i]);
then A3: ex k being Nat st Q[k];
consider k being Nat such that
A4: Q[k] & for k' being Nat st Q[k'] holds k <= k' from Min(A3);
 per cases;
 suppose k = 1;
  hence thesis by A1,A4;
 suppose A5: k <> 1;
    1 - 1 <= k - 1 by A4,REAL_1:49;
  then reconsider k' = k - 1 as Nat by INT_1:16;
  A6: (k - 1) + 1 = (k + (-1)) + 1 by XCMPLX_0:def 8
                  .= k + ((-1) + 1) by XCMPLX_1:1
                  .= k + 0;
  A7: k' <= k' + 1 by NAT_1:29;
    k' <> k' + 1
    proof
    assume A8: k' = k' + 1;
      (k' + 1) - k' = (k' + 1) + (-k') by XCMPLX_0:def 8
                 .= 1 + (k' + (-k')) by XCMPLX_1:1
                 .= 1 + 0 by XCMPLX_0:def 6;
    hence thesis by A8,XCMPLX_1:14;
    end;
  then A9: k' < k by A6,A7,REAL_1:def 5;
  then A10: not(Q[k']) by A4;
    1 < k by A4,A5,REAL_1:def 5;
  then A11: 1 <= k' by A6,NAT_1:38;
    k' < len F() by A4,A9,AXIOMS:22;
  hence thesis by A2,A4,A6,A10,A11;
end;

theorem thsum2: :: thsum2:
for L be add-associative right_zeroed right_complementable (non empty LoopStr),
    r be FinSequence of L
 st len r >= 2 & for k being Nat st 2 < k & k in dom r holds r.k = 0.L
  holds Sum r = r/.1 + r/.2
proof let L be add-associative right_zeroed right_complementable
            (non empty LoopStr), r being FinSequence of L such that
A: len r >= 2 and
B: for k being Nat st 2 < k & k in dom r holds r.k = 0.L;
   now assume r is empty; then r = <*>(the carrier of L);
     then len r = 0 by FINSEQ_1:32;
    hence contradiction by A;
   end; then
   consider a being Element of L, r1 being FinSequence of L such that
D: a = r.1 and
E: r = <*a*>^r1 by FSM_1:5;
Eb: len <*a*> = 1 by FINSEQ_1:57; then
Ea: len r = 1 + len r1 by E, FINSEQ_1:35;
   now assume r1 is empty; then r1 = <*>(the carrier of L);
     then len r1 = 0 by FINSEQ_1:32;
     hence contradiction by A, Ea;
   end; then
   consider b being Element of L, r2 being FinSequence of L such that
F: b = r1.1 and
G: r1 = <*b*>^r2 by FSM_1:5;
Ga: len <*b*> = 1 by FINSEQ_1:57;
H: now let i be Nat such that
   A1: i in dom r2;
   B1: 1+i in dom r1 by A1, G, Ga, FINSEQ_1:41;
       1 <= i by A1, FINSEQ_3:27; then 1 < 1+i by NAT_1:38; then
   C1: 1+1 < 1+(1+i) by REAL_1:67;
   D1: 1+(1+i) in dom r by B1, Eb, E, FINSEQ_1:41;
    thus r2.i = r1.(1+i) by A1, Ga, G, FINSEQ_1:def 7
         .= r.(1+(1+i)) by B1, Eb, E, FINSEQ_1:def 7 .= 0.L by C1, D1, B;
   end; 1 <= len r by A, AXIOMS:22; then
I: 1 in dom r by FINSEQ_3:27;
J: 2 in dom r by A, FINSEQ_3:27;
K: r.2 = r1.(2-1) by E, Eb, A, FINSEQ_1:37 .= r1.1;
  thus Sum r = a + Sum r1 by E, FVSUM_1:89
    .= a + (b + Sum r2) by G, FVSUM_1:89 .= a + (b + 0.L) by H, POLYNOM3:1
   .= a+b by RLVECT_1:def 7 .= r/.1 + b by I, D, FINSEQ_4:def 4
   .= r/.1 + r/.2 by J, K, F, FINSEQ_4:def 4;
end;  

begin :: Canonical ordering of a finite set into a finite sequence

definition
  let A be finite set;
  func canFS(A) -> FinSequence of A means                           :LCFS:
   len it = card A &
   ex f being FinSequence st len f = card A &
    (f.1 = [choose A, A \ {choose A}] or card A = 0) &
    (for i being Nat st 1 <= i & i < card A
      for x being set
       st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}]) &
    for i being Nat st i in dom it holds it.i = (f.i)`1;
  existence proof set cA = card A;
  defpred P[Nat,Function,Function] means
  for x being set
    st $2 = x holds $3 = [choose x`2, x`2 \ {choose x`2}];
P1: for n being Nat st 1 <= n & n < cA
          for x being set ex y being set st P[n,x,y] proof
     let n be Nat such that 1 <= n and n < cA;
     let x be set; take y = [choose x`2, x`2 \ {choose x`2}]; thus thesis;
    end;
P2: for n being Nat st 1 <= n & n < cA
         for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 proof
     let n be Nat such that 1 <= n and n < cA; let x,y1,y2 be set such that
    C1: P[n,x,y1] and D1: P[n,x,y2];
     thus y1 = [choose x`2, x`2 \ {choose x`2}] by C1 .= y2 by D1;
    end;
   consider f being FinSequence such that
A: len f = cA and
B: f.1 = [choose A, A \ {choose A}] or cA = 0 and
C: for n being Nat st 1<=n&n<cA holds P[n,f.n,f.(n+1)] from FinRecEx(P1, P2);
   defpred R[Nat,set] means
   $1 in dom f implies $2 in [: A, bool A :] &
   ex X being finite set st X = ($2)`2  & card X +$1 = cA;
R1: R[1,f.1] proof assume 1 in dom f; then 0+1 <= len f by FINSEQ_3:27; then
         0 < len f by NAT_1:38; then
     C1: cA <> 0 by A; then A <> {} by CARD_1:78; then
     B1: choose A in A;
         A \ {choose A} c= A by XBOOLE_1:36; then A \ {choose A} in bool A;
      hence f.1 in [: A, bool A :] by C1, B, B1, ZFMISC_1:def 2;
      reconsider X = A \ {choose A} as finite set;
      take X; thus X = (f.1)`2 by C1, B, MCART_1:7;
     E1: now assume choose A in A \ {choose A};
          then not choose A in {choose A} by XBOOLE_0:def 4;
          hence contradiction by TARSKI:def 1;
         end;
         {choose A} c= A by B1, ZFMISC_1:37; then
         A = {choose A} \/ (A \ {choose A}) by XBOOLE_1:45;
      hence card X + 1 = cA by E1, CARD_2:54;
    end;
R2: for i being Nat st 1 <= i & i < len f & R[i, f.i] holds R[i+1,f.(i+1)]
    proof let i be Nat such that
    A1: 1 <= i and
    B1: i < len f and
    C1: R[i, f.i] and i+1 in dom f; i <= len f by B1; then
    E1: i in dom f by A1,FINSEQ_3:27; then
    F1: f.i in [: A, bool A :] by C1;
        consider X being finite set such that
    G1: X = (f.i)`2  and
    H1: card X +i = cA by E1, C1;
    H1a: X <> {} by H1, B1, A, CARD_1:78; 
        consider a, ba being set such that a in A and
    J1: ba in bool A and
    K1: f.i = [a, ba] by F1, ZFMISC_1:def 2;
    L1: f.(i+1) = [choose (f.i)`2, (f.i)`2 \ {choose (f.i)`2}] by A,A1,B1,C;
    M1: (f.i)`1 = a & (f.i)`2 = ba by K1, MCART_1:7;
    M1a: (f.i)`2 c= A by M1, J1;
    P1:  choose (f.i)`2 in (f.i)`2 by H1a, G1; then
    N1: choose (f.i)`2 in A by M1a;
        (f.i)`2 \ {choose (f.i)`2} c= (f.i)`2 by XBOOLE_1:36; then
        (f.i)`2 \ {choose (f.i)`2} c= A by M1a, XBOOLE_1:1; then
        (f.i)`2 \ {choose (f.i)`2} in bool A;
     hence f.(i+1) in [: A, bool A :] by N1, L1, ZFMISC_1:def 2;
     reconsider XX = (f.i)`2 \{choose(f.i)`2} as finite set by G1, FINSET_1:16;
     take XX; thus XX = (f.(i+1))`2 by L1, MCART_1:7;
    R1: now assume choose (f.i)`2 in (f.i)`2 \ {choose (f.i)`2};
          then not choose (f.i)`2 in {choose (f.i)`2} by XBOOLE_0:def 4;
          hence contradiction by TARSKI:def 1;
         end;
         {choose (f.i)`2} c= (f.i)`2 by P1, ZFMISC_1:37; then
         (f.i)`2 = {choose (f.i)`2} \/ ((f.i)`2 \ {choose (f.i)`2})
         by XBOOLE_1:45;
       then card X = card XX + 1 by R1, G1, CARD_2:54; 
       then card X +i = card XX + 1 + i;
      hence card XX + (i+1) = cA by H1, XCMPLX_1:1;
    end;
R3: for i being Nat st 1<=i & i <= len f holds R[i,f.i]from IndFinSeq0(R1, R2);
   rng f c= [: A, bool A :] proof let y be set; assume y in rng f; then
      consider i being Nat such that
   A1: i in dom f and
   B1: y = f.i by FINSEQ_2:11;       1 <= i & i <= len f by A1, FINSEQ_3:27;
    hence thesis by B1, A1, R3;
   end; then reconsider f as FinSequence of [: A, bool A :] by FINSEQ_1:def 4;
   deffunc F(Nat) = (f.$1)`1;
   consider p being FinSequence such that
D: len p = card A and
E: for k being Nat st k in Seg card A holds p.k = F(k) from SeqLambda;
F: dom p = Seg card A by D, FINSEQ_1:def 3;
G: dom p = dom f by D, A, FINSEQ_3:31;
   rng p c= A proof let y be set; assume y in rng p; then
      consider i being Nat such that
   A1: i in dom p and
   B1: p.i = y by FINSEQ_2:11;
   E1: p.i = (f.i)`1 by A1, F, E;
     f.i in [:A, bool A:] by A1,G,FINSEQ_2:13; then(f.i)`1 in A by MCART_1:10;
    hence y in A by B1, E1;
   end; then reconsider p as FinSequence of A by FINSEQ_1:def 4;
   take p; thus len p = card A by D;
   take f; thus thesis by A, B, C, E, F;
  end;
  uniqueness proof let it1, it2 be FinSequence of A such that
  A1: len it1 = card A; given f being FinSequence such that
  B1a: len f = card A and
  B1: f.1 = [choose A, A \ {choose A}] or card A = 0 and
  C1: for i being Nat st 1 <= i & i < card A
          holds for x being set
           st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}] and
  D1: for i being Nat st i in dom it1 holds it1.i = (f.i)`1;
      assume
  A2: len it2 = card A; given g being FinSequence such that
  B2a: len g = card A and
  B2: g.1 = [choose A, A \ {choose A}] or card A = 0 and
  C2: for i being Nat st 1 <= i & i < card A
          holds for x being set 
           st g.i = x holds g.(i+1) = [choose x`2, x`2 \ {choose x`2}] and
  D2: for i being Nat st i in dom it2 holds it2.i = (g.i)`1;
  defpred Q[Nat,set] means card A <> 0 implies $2 = g.$1;
Q1: Q[1, f.1] by B1, B2;
Q2: for i being Nat st 1 <= i & i < len f & Q[i, f.i] holds Q[i+1, f.(i+1)]
    proof let i be Nat such that
    A3: 1 <= i and
    B3: i < len f and
    D3: Q[i, f.i] and
    E3: card A <> 0;        set x = f.i;
     thus f.(i+1) = [choose x`2, x`2 \ {choose x`2}] by B1a, A3, B3, C1
         .= g.(i+1) by E3, D3, A3, B3, B1a, C2;
    end;
Q3: for i being Nat st 1<=i & i<=len f holds Q[i, f.i] from IndFinSeq0(Q1,Q2);
  E2: f = g proof
       per cases;
       suppose S1: card A = 0;
        thus f = {} by S1, B1a, FINSEQ_1:25 .= g by S1, B2a, FINSEQ_1:25;
       suppose S1: card A <> 0;
       now let j be Nat; assume j in Seg len f;
          then j in dom f by FINSEQ_1:def 3; then
          1 <= j & j <= len f by FINSEQ_3:27;
         hence f.j = g.j by S1, Q3;
       end;
       hence f = g by B1a, B2a, FINSEQ_2:10;
      end;
    now let j be Nat such that
    A3: j in Seg card A;
    B3: dom it1 = dom it2 by A1, A2, FINSEQ_3:31;
    C3: dom it1 = Seg card A by A1, FINSEQ_1:def 3;
      thus it1.j = (f.j)`1 by D1, C3, A3 .= it2.j by E2, D2, A3, B3, C3;
    end;
   hence it1 = it2 by A1, A2, FINSEQ_2:10;
  end;
end;

theorem CFS0: :: CFS0:
for A being finite set holds canFS(A) is one-to-one
proof let A be finite set;
 set F = canFS(A), cA = card A;
A: len F = card A by LCFS;
   consider f being FinSequence such that
B: len f = cA and
C: f.1 = [choose A, A \ {choose A}] or card A = 0 and
D: for i being Nat st 1 <= i & i < cA
    for x being set
     st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}] and
E: for i being Nat st i in dom F holds F.i = (f.i)`1 by LCFS;
 per cases;
 suppose A = {};  then card A = 0 by CARD_1:78; then F = {} by A, FINSEQ_1:25;
  hence canFS(A) is one-to-one;
 suppose S1: A <> {}; then
Z: card A <> 0 by GRAPH_5:5; then card A > 0 by NAT_1:19; then
Y: 0+1 <= len F by A, NAT_1:38;
X: 1 in dom F by Y, FINSEQ_3:27;
 defpred P[Nat, set] means
  rng (F| Seg $1) /\ ($2)`2 = {} &
  (ex X being finite set st X = ($2)`2  & card X +$1 = cA) &
  ($1 < len F implies not F.($1+1) in rng (F| Seg $1));
P1: P[1, f.1] proof
     B1: choose A in A by S1;
         reconsider F1 = (F | Seg 1) as FinSequence of A by FINSEQ_1:23;
         1 <= len F by X, FINSEQ_3:27; then
         consider a being Element of A such that
     C1b: F1 = <* a *> by S1, QC_LANG4:7;
     C1a: len F1 = 1 by C1b, FINSEQ_1:56;
         1 in Seg (0+1) by FINSEQ_1:6; then
         F1.1 = F.1 by FUNCT_1:72 .= (f.1)`1 by X, E
             .= choose A by Z, C, MCART_1:7; then
         F | Seg 1 = <* choose A *> by C1a, FINSEQ_1:57; then
     D1: rng (F| Seg 1) = {choose A} by FINSEQ_1:56;
     E1: (f.1)`2 = A \ {choose A} by Z, C, MCART_1:7;
      thus rng (F| Seg 1) /\ (f.1)`2 = {} proof assume not thesis; then
      consider x being set such that
      A2: x in rng (F| Seg 1) /\ (f.1)`2 by XBOOLE_0:def 1;
          x in {choose A} & x in (f.1)`2 by A2, D1, XBOOLE_0:def 3;
       hence contradiction by E1, XBOOLE_0:def 4;
      end;
      now reconsider X = A \ {choose A} as finite set;
       take X; thus X = (f.1)`2 by C, Z, MCART_1:7;
      E1: now assume choose A in A \ {choose A};
          then not choose A in {choose A} by XBOOLE_0:def 4;
          hence contradiction by TARSKI:def 1;
         end;
         {choose A} c= A by B1, ZFMISC_1:37; then
         A = {choose A} \/ (A \ {choose A}) by XBOOLE_1:45;
       hence card X + 1 = cA by E1, CARD_2:54;
      end;
     hence ex X being finite set st X = (f.1)`2  & card X +1 = cA; then
         consider X being finite set such that
     H1: X = (f.1)`2  and
     I1: card X +1 = cA;
     J1: 1 < len F implies (f.1)`2 <> {} by H1, CARD_1:78, I1, A;
      assume
      Aa: 1 < len F; then 1+1 <= len F by NAT_1:38; then
         1+1 in dom F by FINSEQ_3:27; then
      A2: F.2 = (f.2)`1 by E;
          f.(1+1) = [choose (f.1)`2, (f.1)`2 \ {choose (f.1)`2}]
            by Aa, A, D; then
      C2: (f.(1+1))`1 = choose (A \ {choose A}) by E1, MCART_1:7;
         thus not F.(1+1) in rng (F| Seg 1)
             by A2,C2,D1,Aa,J1,E1,XBOOLE_0:def 4;
    end;
P2: for i being Nat st 1 <= i & i < len f & P[i, f.i] holds P[i+1, f.(i+1)]
    proof let i be Nat such that
    A1: 1 <= i and
    B1: i < len f and
    C1: P[i, f.i];
    D1: rng (F| Seg i) /\ (f.i)`2 = {} by C1;
        consider X being finite set such that
    G1: X = (f.i)`2  and
    H1: card X +i = cA by C1;
    L1: f.(i+1) = [choose (f.i)`2, (f.i)`2 \ {choose (f.i)`2}] by A1,B1,B,D;
    M1: (f.i)`2 is non empty by H1, G1, B1, B, CARD_1:78;
        {choose (f.i)`2} c= (f.i)`2 by M1, ZFMISC_1:37; then
    M1a: (f.i)`2={choose (f.i)`2}\/((f.i)`2 \ {choose (f.i)`2}) by XBOOLE_1:45;
    N1: i+1 <= len F by B1, A, B, NAT_1:38;
        1 <= i+1 by NAT_1:37; then
    N1a: i+1 in dom F by N1, FINSEQ_3:27;
        reconsider Fi = F| Seg i, Fi1 = F| Seg (i+1) as FinSequence of A
          by FINSEQ_1:23;
        consider a being Element of A such that
    O1: Fi1 = Fi^<*a*> by N1, S1, QC_LANG4:6;
    P1: rng Fi1 = rng Fi \/ rng <*a*> by O1, FINSEQ_1:44
               .= rng Fi \/ {a} by FINSEQ_1:56;
        i+1 in Seg (i+1) by FINSEQ_1:6; then
    P1a: F.(i+1) = Fi1.(i+1) by FUNCT_1:72;
         i = len Fi by B1, A, B, FINSEQ_1:21; then
         Fi1.(i+1) = a by O1, FINSEQ_1:59; then
    R1: a = F.(i+1) by P1a .= (f.(i+1))`1 by N1a, E
           .= choose (f.i)`2 by L1, MCART_1:7;
    T1: (f.(i+1))`2 = (f.i)`2 \ {a} by L1, R1, MCART_1:7;
    thus
    Z1: rng (F| Seg (i+1)) /\ (f.(i+1))`2 = {} proof assume not thesis;
     then consider x being set such that
    A2: x in (rng Fi \/ {a}) /\ ((f.i)`2 \ {a}) by P1, T1, XBOOLE_0:def 1;
        x in (rng Fi \/ {a}) & x in ((f.i)`2 \ {a}) by A2, XBOOLE_0:def 3; then
        (x in rng Fi or x in {a}) & (x in (f.i)`2 & not x in {a})
              by XBOOLE_0:def 2, XBOOLE_0:def 4; then
        (x in rng Fi) & x in (f.i)`2; then
        x in rng (F| Seg i) /\ (f.i)`2 by XBOOLE_0:def 3;        
     hence contradiction by D1;
    end;
     now reconsider XX = (f.i)`2 \{choose(f.i)`2} as finite set
             by G1,FINSET_1:16;
     take XX; thus XX = (f.(i+1))`2 by L1, MCART_1:7;
      now assume choose (f.i)`2 in (f.i)`2 \ {choose (f.i)`2};
          then not choose (f.i)`2 in {choose (f.i)`2} by XBOOLE_0:def 4;
          hence contradiction by TARSKI:def 1;
         end;
       then card X = card XX + 1 by M1a, G1, CARD_2:54; 
       then card X +i = card XX + 1 + i;
      hence card XX + (i+1) = cA by H1, XCMPLX_1:1;
     end;
    hence
    V1: ex X being finite set st X = (f.(i+1))`2  & card X +(i+1) = cA;
    assume
    A2: i+1 < len F;     consider X being finite set such that
    V2: X = (f.(i+1))`2  and
    W2: card X +(i+1) = cA by V1;
    U1: (f.(i+1))`2 <> {} by V2, CARD_1:78, W2, A2, A;
    B2: 1 <= i+1 by NAT_1:37;        set i1 = i+1;
    D2: 1 <= i1+1 by NAT_1:37;       i1+1 <= len F by A2, NAT_1:38; then
        i1+1 in dom F by D2, FINSEQ_3:27; then
    G2: F.(i1+1) = (f.(i1+1))`1 by E;
        f.(i1+1) = [choose (f.i1)`2, (f.i1)`2 \ {choose (f.i1)`2}]
        by A2,B2,A,D; then
    I2: (f.(i1+1))`1 = choose (f.i1)`2 by MCART_1:7;
    assume
    K2: F.((i+1)+1) in rng (F| Seg (i+1));
        choose (f.i1)`2 in (f.i1)`2 by U1; then
        choose (f.i1)`2 in (rng Fi1 /\ (f.i1)`2) by K2, G2, I2, XBOOLE_0:def 3;
     hence contradiction by Z1;
    end;
P3: for i being Nat st 1<=i & i<=len f holds P[i, f.i] from IndFinSeq0(P1,P2);
  thus canFS(A) is one-to-one proof let i, j be set such that
H: i in dom F and
I: j in dom F and
J: F.i = F.j;
Fd: dom F = Seg len F by FINSEQ_1:def 3;
   per cases;
   suppose i = j;
    hence thesis;
   suppose S1: i <> j; reconsider i, j as Nat by H, I, FINSEQ_3:25;
K: 1 <= i & i <= len F by H, FINSEQ_3:27;
L: 1 <= j & j <= len F by I, FINSEQ_3:27;
   now 
   per cases by S1, REAL_1:def 5;
    suppose S2: i < j; j <> 0 by L; then consider j1 being Nat such that
  A2: j = j1+1 by NAT_1:22;
  B2: j1 < len F by L, A2, NAT_1:38;
  C2: j1 <= len F by B2;       i+1 <= j by S2, NAT_1:38; then
  C2b: i <= j1 by A2, REAL_1:53; then       1 <= j1 by K, AXIOMS:22; then
  D2: not F.(j1+1) in rng (F|Seg j1) by B2, P3, A, B;
  E2: i in Seg j1 by K, C2b, FINSEQ_1:3;
  F2: (F|Seg j1).i = F.i by E2, FUNCT_1:72;
      Seg j1 c= dom F by C2, Fd, FINSEQ_1:7; then
      dom (F|Seg j1) = Seg j1 by RELAT_1:91; then
      i in dom (F|Seg j1) by E2; then F.i in rng (F|Seg j1) by F2, FUNCT_1:12;
     hence contradiction by D2, A2, J;    
    suppose S2: i > j;
      i <> 0 by K; then
        consider i1 being Nat such that
  A2: i = i1+1 by NAT_1:22;
  B2: i1 < len F by K, A2, NAT_1:38;
  C2: i1 <= len F by B2;       j+1 <= i by S2, NAT_1:38; then
  C2b: j <= i1 by A2, REAL_1:53; then       1 <= i1 by L, AXIOMS:22; then
  D2: not F.(i1+1) in rng (F|Seg i1) by B2, P3, A, B;
  E2: j in Seg i1 by L, C2b, FINSEQ_1:3;
  F2: (F|Seg i1).j = F.j by E2, FUNCT_1:72;
      Seg i1 c= dom F by C2, Fd, FINSEQ_1:7; then
      dom (F|Seg i1)=Seg i1 by RELAT_1:91; then j in dom (F|Seg i1) by E2;then
      F.j in rng (F|Seg i1) by F2, FUNCT_1:12;
     hence contradiction by D2, A2, J;
   end;
    hence thesis;
  end;
end;

theorem CFS1: :: CFS1:
for A being finite set holds rng canFS(A) = A
proof let A be finite set; set F = canFS(A), cA = card A;
A: len F = card A by LCFS;
   consider f being FinSequence such that
B: len f = cA and
C: f.1 = [choose A, A \ {choose A}] or card A = 0 and
D: for i being Nat st 1 <= i & i < cA
    for x being set
     st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}] and
E: for i being Nat st i in dom F holds F.i = (f.i)`1 by LCFS;
 per cases;
 suppose S1: A = {}; then   card A = 0 by CARD_1:78; then
   F = {} by A, FINSEQ_1:25;
  hence thesis by S1, FINSEQ_1:27;
 suppose S1: A <> {}; then
Z: card A <> 0 by GRAPH_5:5; then   card A > 0 by NAT_1:19; then
Y: 0+1 <= len F by A, NAT_1:38;
X: 1 in dom F by Y, FINSEQ_3:27;
 defpred P[Nat, set] means
 rng (F| Seg $1) \/ ($2)`2 = A &
 ex X being finite set st X = ($2)`2  & card X +$1 = cA;
P1: P[1, f.1] proof
     B1: choose A in A by S1;
         reconsider F1 = (F | Seg 1) as FinSequence of A by FINSEQ_1:23;
         1 <= len F by X, FINSEQ_3:27; then
     consider a being Element of A such that
     C1b: F1 = <* a *> by S1, QC_LANG4:7;
     C1a: len F1 = 1 by C1b, FINSEQ_1:56;   1 in Seg (0+1) by FINSEQ_1:6; then
         F1.1 = F.1 by FUNCT_1:72
                  .= (f.1)`1 by X, E .= choose A by Z, C, MCART_1:7; then
         F | Seg 1 = <* choose A *> by C1a, FINSEQ_1:57; then
     D1: rng (F| Seg 1) = {choose A} by FINSEQ_1:56;
     E1: (f.1)`2 = A \ {choose A} by Z, C, MCART_1:7;
         {choose A} c= A by B1, ZFMISC_1:37; 
      hence rng (F| Seg 1) \/ (f.1)`2 = A by D1, E1, XBOOLE_1:45;
      reconsider X = A \ {choose A} as finite set;
      take X;      thus X = (f.1)`2 by C, Z, MCART_1:7;
     E1: now assume choose A in A \ {choose A};
          then not choose A in {choose A} by XBOOLE_0:def 4;
          hence contradiction by TARSKI:def 1;
         end;
         {choose A} c= A by B1, ZFMISC_1:37; then
         A = {choose A} \/ (A \ {choose A}) by XBOOLE_1:45;
      hence card X + 1 = cA by E1, CARD_2:54;
    end;
P2: for i being Nat st 1 <= i & i < len f & P[i, f.i] holds P[i+1, f.(i+1)]
    proof let i be Nat such that
    A1: 1 <= i and
    B1: i < len f and
    C1: P[i, f.i];
    D1: rng (F| Seg i) \/ (f.i)`2 = A by C1;
        consider X being finite set such that
    G1: X = (f.i)`2  and
    H1: card X +i = cA by C1;
    L1: f.(i+1) = [choose (f.i)`2, (f.i)`2 \ {choose (f.i)`2}] by A1,B1,B,D;
    M1: (f.i)`2 is non empty by H1, G1, B1, B, CARD_1:78;
        {choose (f.i)`2} c= (f.i)`2 by M1, ZFMISC_1:37; then
    M1a: (f.i)`2 = {choose (f.i)`2} \/ ((f.i)`2 \ {choose (f.i)`2})
         by XBOOLE_1:45;
    N1: i+1 <= len F by B1, A, B, NAT_1:38;
        1 <= i+1 by NAT_1:37; then
    N1a: i+1 in dom F by N1, FINSEQ_3:27;
        reconsider Fi = F| Seg i, Fi1 = F| Seg (i+1) as FinSequence of A
          by FINSEQ_1:23;
        consider a being Element of A such that
    O1: Fi1 = Fi^<*a*> by N1, S1, QC_LANG4:6;
    P1: rng Fi1 = rng Fi \/ rng <*a*> by O1, FINSEQ_1:44
               .= rng Fi \/ {a} by FINSEQ_1:56;
        i+1 in Seg (i+1) by FINSEQ_1:6; then
    P1a: F.(i+1) = Fi1.(i+1) by FUNCT_1:72;
         i = len Fi by B1, A, B, FINSEQ_1:21; then
         Fi1.(i+1) = a by O1, FINSEQ_1:59; then
    R1: a = F.(i+1) by P1a .= (f.(i+1))`1 by N1a, E
           .= choose (f.i)`2 by L1, MCART_1:7;
    T1: (f.(i+1))`2 = (f.i)`2 \ {a} by L1, R1, MCART_1:7;
         rng Fi1 \/ (f.(i+1))`2
       = rng Fi \/ ({a} \/ ((f.i)`2 \ {a})) by T1, P1, XBOOLE_1:4;
    hence rng (F| Seg (i+1)) \/ (f.(i+1))`2 = A by M1a, D1, R1;
     reconsider XX = (f.i)`2 \{choose(f.i)`2} as finite set by G1, FINSET_1:16;
     take XX;
     thus XX = (f.(i+1))`2 by L1, MCART_1:7;
        now assume choose (f.i)`2 in (f.i)`2 \ {choose (f.i)`2};
          then not choose (f.i)`2 in {choose (f.i)`2} by XBOOLE_0:def 4;
          hence contradiction by TARSKI:def 1;
         end;
       then card X = card XX + 1 by M1a, G1, CARD_2:54; 
       then card X +i = card XX + 1 + i;
      hence card XX + (i+1) = cA by H1, XCMPLX_1:1;
    end;
P3: for i being Nat st 1<=i & i<=len f holds P[i, f.i] from IndFinSeq0(P1,P2);
   now assume len F < 1; then len F = 0 by RLVECT_1:98;
    hence contradiction by S1, A, GRAPH_5:5;
   end; then
F: 1 <= len F;
G: F = F | (Seg len F) by FINSEQ_3:55;
H: rng F \/ (f.len F)`2 = A by F, G, A, B, P3;
   consider X being finite set such that
I: X = (f.len F)`2  and
J: card X + len f = cA by F, A, B, P3;
   card X = 0 by J, B, XCMPLX_1:3; then
   X = {} by GRAPH_5:5; then
   X c= rng F by XBOOLE_1:2;
 hence rng canFS(A) = A by H, I, XBOOLE_1:12;
end;

theorem CFS2: :: CFS2:
for a being set holds canFS({a}) = <* a *>
proof let a be set;
A: len canFS({a}) = card {a} by LCFS .= 1 by CARD_1:79;
   rng canFS({a}) = {a} by CFS1;
 hence canFS({a}) = <* a *> by A, FINSEQ_1:56;
end;

theorem CFS3: :: CFS3:
for A being finite set holds (canFS A)" is Function of A, Seg card A
proof let A be finite set;
A: canFS A is one-to-one by CFS0;
   len canFS A = card A by LCFS; then
C: dom canFS A = Seg card A by FINSEQ_1:def 3;
   rng canFS A = A by CFS1; then
D: dom ((canFS A)") = A by A, FUNCT_1:55;
   rng ((canFS A)") = Seg card A by A, C, FUNCT_1:55;
 hence (canFS A)" is Function of A, Seg card A by D, FUNCT_2:3;
end;

begin :: More about bags

definition
let X be set, S be finite Subset of X, n be Nat;
func (S, n)-bag -> Element of Bags X equals    :BAG2:
 (EmptyBag X) +* (S --> n);
 correctness proof
   set b = (EmptyBag X) +* (S --> n);
 E: dom (S --> n) = S by FUNCOP_1:19;
 D: EmptyBag X = (X --> 0) by POLYNOM1:def 15;
 C: dom b = dom (EmptyBag X) \/ dom (S --> n) by FUNCT_4:def 1
         .= X \/ dom (S --> n) by D, FUNCOP_1:19 .= X \/ S by FUNCOP_1:19
         .= X by XBOOLE_1:12;
    rng (EmptyBag X) c= {0} & rng (S-->n) c= {n} by D, FUNCOP_1:19; then
 F: rng (EmptyBag X) \/ rng (S --> n) c= {0} \/ {n} by XBOOLE_1:13;
 G: {0} c= NAT by ZFMISC_1:37;
 H: {n} c= NAT by ZFMISC_1:37;
 I: {0} \/ {n} c= NAT by G, H, XBOOLE_1:8;
    rng b c= rng (EmptyBag X) \/ rng (S --> n) by FUNCT_4:18; then
    rng b c= {0} \/ {n} by F, XBOOLE_1:1; then
    rng b c= NAT by I, XBOOLE_1:1 ; then
 A: b is natural-yielding by SEQM_3:def 8;
 J: now let i be set such that
    A: not i in S;
      thus b.i = (EmptyBag X).i by A, E, FUNCT_4:12 .= 0 by POLYNOM1:56;
    end;
 K: now let i be set such that A: i in S;
      thus b.i = (S --> n).i by A, E, FUNCT_4:14 .= n by A, FUNCOP_1:13;    
    end;
    support b is finite proof
     per cases;
     suppose S1: S is empty;
       now assume support b is non empty; then consider x being set such that
       A1: x in support b by XBOOLE_0:def 1;
           b.x <> 0 by A1, POLYNOM1:def 7; then x in S by J; 
        hence contradiction by S1;
       end; 
      hence support b is finite;
     suppose S1:  S is non empty & n = 0;
       now assume support b is non empty; then consider x being set such that
       A1: x in support b by XBOOLE_0:def 1;
       C1: b.x <> 0 by A1, POLYNOM1:def 7; then
       B1: x in S by J; then
           b.x = (S-->n).x by E, FUNCT_4:14 .= 0 by S1, B1, FUNCOP_1:13;
        hence contradiction by C1;
       end; 
      hence support b is finite;
     suppose A: S is non empty & n <> 0;
       for x being set holds x in S iff b.x <> 0 by A, J, K;
       then support b = S by POLYNOM1:def 7;
      hence support b is finite;
    end; then
    b is finite-support by POLYNOM1:def 8;
   then (EmptyBag X) +* (S --> n) is bag of X by A, C, PBOOLE:def 3; 
  hence (EmptyBag X) +* (S --> n) is Element of Bags X by POLYNOM1:def 14;
 end;
end;

Snbagdom:
for X being set, S being finite Subset of X, n being Nat
 holds dom (S, n)-bag = X by PBOOLE:def 3;

theorem Snbag0: :: Snbag0:
for X being set, S being finite Subset of X, n being Nat, i being set
 st not i in S holds (S, n)-bag.i = 0
proof let X be set, S be finite Subset of X, n be Nat, i be set such that
A: not i in S;
B: dom (S --> n) = S by FUNCOP_1:19;
   (S, n)-bag = (EmptyBag X) +* (S --> n) by BAG2;
 hence (S, n)-bag.i = (EmptyBag X).i by A, B, FUNCT_4:12 .= 0 by POLYNOM1:56;
end;

theorem Snbag1: :: Snbag1:
for X being set, S being finite Subset of X, n being Nat, i being set
 st i in S holds (S, n)-bag.i = n
proof let X be set, S be finite Subset of X, n be Nat, i be set such that
A: i in S;
B: dom (S --> n) = S by FUNCOP_1:19;
   (S, n)-bag = (EmptyBag X) +* (S --> n) by BAG2;
 hence (S, n)-bag.i = (S --> n).i by A, B, FUNCT_4:14 .= n by A, FUNCOP_1:13;
end;

theorem Snbagsup: :: Snbagsup:
for X being set, S being finite Subset of X, n being Nat
 st n <> 0 holds support (S, n)-bag = S
proof let X be set, S be finite Subset of X, n be Nat; assume n <> 0; then
   for x being set holds x in S iff (S, n)-bag.x <> 0 by Snbag0, Snbag1;
 hence support (S, n)-bag = S by POLYNOM1:def 7;
end;

theorem :: Snbage: :: :: Snbage:
for X being set, S being finite Subset of X, n being Nat
 st S is empty or n = 0 holds (S, n)-bag = EmptyBag X
proof let X be set, S be finite Subset of X, n be Nat such that
A: S is empty or n = 0;
   now let i be set; assume i in X;
    per cases;
    suppose S1: i in S; then n = 0 by A;
     hence (S, n)-bag.i = 0 by S1, Snbag1 .= (EmptyBag X).i by POLYNOM1:56;
    suppose not i in S;
     hence (S, n)-bag.i = 0 by Snbag0 .= (EmptyBag X).i by POLYNOM1:56;
   end; 
 hence (S, n)-bag = EmptyBag X by PBOOLE:3;
end;
  
theorem Snbagsum: :: Snbagsum:
for X being set, S, T being finite Subset of X, n being Nat
 st S misses T holds (S \/ T, n)-bag = (S,n)-bag + (T,n)-bag
proof let X be set, S, T be finite Subset of X, n be Nat; assume
   S misses T; then
AA: S /\ T = {} by XBOOLE_0:def 7;
   now let i be set such that i in X;
    per cases by XBOOLE_0:def 2;
    suppose
    B: not i in S \/ T; then
    C: not i in S & not i in T by XBOOLE_0:def 2;
     thus (S \/ T, n)-bag.i = 0 by B, Snbag0 .= (S,n)-bag.i + 0 by C, Snbag0
       .= (S,n)-bag.i + (T,n)-bag.i by C, Snbag0
       .= ((S,n)-bag + (T,n)-bag).i by POLYNOM1:def 5;
    suppose
    B: i in S; then
    C: i in S \/ T by XBOOLE_0:def 2;
    D: not i in T by B, AA, XBOOLE_0:def 3;
     thus (S \/ T, n)-bag.i = n by C, Snbag1
       .= (S,n)-bag.i + 0 by B, Snbag1 .= (S,n)-bag.i +(T,n)-bag.i by D, Snbag0
       .= ((S,n)-bag + (T,n)-bag).i by POLYNOM1:def 5;
    suppose
    B: i in T;  then
    C: i in S \/ T by XBOOLE_0:def 2;
    D: not i in S by B, AA, XBOOLE_0:def 3;
     thus (S \/ T, n)-bag.i = n by C, Snbag1 .= (T,n)-bag.i + 0 by B, Snbag1
       .= (S,n)-bag.i + (T,n)-bag.i by D, Snbag0
       .= ((S,n)-bag + (T,n)-bag).i by POLYNOM1:def 5;
   end;
 hence (S \/ T, n)-bag = (S,n)-bag + (T,n)-bag by PBOOLE:3;
end;
 
definition
  let A be set, b be bag of A;
  func degree b -> Nat means                                          :LBAGDEG:
  ex f being FinSequence of NAT st it = Sum f & f = b*canFS(support b);
  existence proof set cS = canFS(support b);
   set f = b*cS;
  A: rng b c= NAT by SEQM_3:def 8;
  Aa: support b c= dom b by POLYNOM1:41; rng cS = support b by CFS1;
     then rng cS c= dom b by Aa; then dom f = dom cS by RELAT_1:46;
     then dom f = Seg len cS by FINSEQ_1:def 3; then
  B: f is FinSequence by FINSEQ_1:def 2;
     rng f c= rng b by RELAT_1:45; then rng f c= NAT by A, XBOOLE_1:1; then
   reconsider f as FinSequence of NAT by B, FINSEQ_1:def 4;
   take S = Sum f; thus thesis;
  end;
  uniqueness;
end;

theorem BAGDEG0: :: BAGDEG0:
for A being set, b being bag of A holds b = EmptyBag A iff degree b = 0
proof let A be set, b be bag of A;
  set cS = canFS(support b);
  hereby assume b = EmptyBag A;  then support b = {} by BAGORDER:19; then
      len cS = 0 by LCFS, CARD_1:78; then cS = <*>NAT by FINSEQ_1:32; then
  D1: b*cS = <*>NAT by RELAT_1:62; set f = <*>NAT; Sum f = 0 by RVSUM_1:102;
    hence degree b = 0 by D1, LBAGDEG;
  end;
  assume A: degree b = 0;
     consider f being FinSequence of NAT such that
  B: degree b = Sum f and
  C: f = b*canFS(support b) by LBAGDEG;
     now assume
     A1: support b <> {};  f is FinSequence of REAL by FINSEQ_2:27; then
     B1: f is Element of (len f)-tuples_on REAL by FINSEQ_2:110;
     C1: for i be Nat st i in dom f holds 0 <= f.i by NAT_1:18;
         now consider x being set such that
         A2: x in support b by A1, XBOOLE_0:def 1;
             x in rng cS by A2, CFS1; then consider i being Nat such that
         B2: i in dom cS and
         C2: cS.i = x by FINSEQ_2:11;
             support b c= dom b by POLYNOM1:41; then x in dom b by A2; then
         E2: i in dom f by B2, C2, C, FUNCT_1:21; 
             f.i = b.(cS.i) by B2, C, FUNCT_1:23; then
             f.i <> 0 by A2, C2, POLYNOM1:def 7; then  0 < f.i by NAT_1:19;
          hence ex i being Nat st i in dom f & 0 < f.i by E2;
         end; then
         0 < Sum f by C1, B1, RVSUM_1:115; 
       hence contradiction by A, B;
     end;
  hence b = EmptyBag A by BAGORDER:20;
end;

theorem BAGDEG1: :: BAGDEG1:
for A being set, S being finite Subset of A, b being bag of A 
 holds S = support b & degree b = card S iff b = (S, 1)-bag
proof let A be set, S be finite Subset of A, b be bag of A;
  set cS = canFS(S);    set f = b*cS;
A: rng cS = S by CFS1;
B: dom b = A by PBOOLE:def 3; then rng cS c= dom b by A; then
C: dom f = dom cS by RELAT_1:46; then
D: dom f = Seg len cS by FINSEQ_1:def 3; then
   reconsider f as FinSequence by FINSEQ_1:def 2;
Da: len cS = card S by LCFS;
E: rng cS = S by CFS1;
F: len cS = len f by C, FINSEQ_3:31;
   rng f c= NAT proof let y be set; assume y in rng f; then
      consider x being set such that
   A1: x in dom f and
   B1: y = f.x by FUNCT_1:def 5;
   C1: cS.x in dom b by A1, FUNCT_1:21;
   D1: rng b c= NAT by SEQM_3:def 8;
       f.x = b.(cS.x) by A1, FUNCT_1:22; then f.x in rng b by C1, FUNCT_1:12;
    hence y in NAT by B1, D1;
   end; then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
 hereby assume that
 C1: S = support b and
 D1: degree b = card S;
     consider F being FinSequence of NAT such that
 E1: degree b = Sum F and
 F1: F = b*cS by C1, LBAGDEG;
 G1: len F = card S by F1, Da, F;
     now let i be Nat; assume
     A2: i in dom F; then
     B2: F.i = b.(cS.i) by F1, FUNCT_1:22;
         i in dom cS by A2, F1, C; then cS.i in rng cS by FUNCT_1:12;
       hence F.i <> 0 by A, C1, B2, POLYNOM1:def 7;
     end; then
 H1: F = len F |-> 1 by G1, E1, D1, SumFS;
     set sb = (S, 1)-bag;
 G1: support b = support sb by C1, Snbagsup;
     now
      thus dom b = dom sb by B, Snbagdom;
      let x be set; assume x in dom b;
      per cases;
      suppose S1: x in support b;
      F2: cS is one-to-one by CFS0;
      E2: rng cS = support b by A, C1; then
      D2: cS".x in dom cS by S1, F2, FUNCT_1:54;
      B2: cS".x in Seg len F by C, F1, D2, FINSEQ_1:def 3;
      C2: cS.(cS".x) = x by S1, E2, F2, FUNCT_1:57;
       thus b.x = b.(cS.(cS".x)) by C2 .= F.(cS".x) by F1, D2, FUNCT_1:23
               .= 1 by B2, H1, FINSEQ_2:70 .= sb.x by S1, C1, Snbag1;
      suppose S1: not x in support b; 
       hence b.x = 0 by POLYNOM1:def 7 .= sb.x by S1, G1, POLYNOM1:def 7;      
     end;
  hence b = (S, 1)-bag by FUNCT_1:9;
 end;
 assume
 A1: b = (S, 1)-bag;
 hence
 C1: S = support b by Snbagsup;
 D1: degree b = Sum f by C1, LBAGDEG;  set g = (card S) |-> 1;
   now
    thus len f = card S by C, Da, FINSEQ_3:31;
    thus len g = card S by FINSEQ_2:69;
    let i be Nat; assume
   D1: i in Seg card S;
   E1: cS.i in S by D1, C, D, Da, E, FUNCT_1:12;
    thus f.i = b.(cS.i) by D, Da, D1, FUNCT_1:22
            .= 1 by A1, E1, Snbag1 .= g.i by D1, FINSEQ_2:70;
   end; then f = g by FINSEQ_2:10; 
 hence degree b = (card S)*1 by D1, RVSUM_1:110 .= card S;
end;

theorem BAGDEG2c: :: BAGDEG2c:
for A being set, S being finite Subset of A, b being bag of A
 st support b c= S
  ex f being FinSequence of NAT st f = b*canFS(S) & degree b = Sum f
proof let A be set, S be finite Subset of A, b be bag of A such that
A: support b c= S;   set cS = canFS(S); set f = b*cS;
   len cS = card S by LCFS; then
B: dom cS = Seg card S by FINSEQ_1:def 3;
C: rng cS = S by CFS1;
Ca: cS is one-to-one by CFS0;
D: dom b = A by PBOOLE:def 3; then
E: dom f = Seg card S by B, C, RELAT_1:46; then
   reconsider f as FinSequence by FINSEQ_1:def 2;
F: rng b c= NAT by SEQM_3:def 8;
   rng f c= rng b by RELAT_1:45; then rng f c= NAT by F, XBOOLE_1:1; then
   reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
   take f; thus f = b*canFS(S);
   set cs = canFS(support b);
Ga: cs is one-to-one by CFS0;
   consider g being FinSequence of NAT such that
G: degree b = Sum g and
H: g = b*cs by LBAGDEG;    len cs = card support b by LCFS; then
Hb: dom cs = Seg card support b by FINSEQ_1:def 3;
Hc: rng cs = support b by CFS1;    support b c= A by A, XBOOLE_1:1; then
Hd: dom g = Seg card support b by H, Hb, Hc, D, RELAT_1:46; then
Ha: len g = card support b by FINSEQ_1:def 3;
I: card support b <= card S by A, CARD_1:80;
 per cases by I, REAL_1:def 5;
 suppose
 SU: card support b < card S; then consider d being Nat such that
 J: card S = (card support b) + d and 1 <= d by FSM_1:1;
    set h = d |-> (0 qua Real);
 Kb: len h = d by FINSEQ_2:69; then
 Kc: dom h = Seg d by FINSEQ_1:def 3;
    reconsider gr = g, fr = f as FinSequence of REAL by FINSEQ_2:27;
    set F = gr^h;
    len F = len g + len h by FINSEQ_1:35 .= card S by J, Kb, Ha; then
 Ka: dom F = Seg card S by FINSEQ_1:def 3;
    set dd = {j where j is Nat : j in dom f & f.j = 0};
 M: now support b <> S by SU; then consider x being set such that
    B1: not (x in support b iff x in S) by TARSKI:2;
        x in support b implies x in S by A; then
    C1: not x in support b & x in S by B1; then consider j being set such that
    D1: j in dom cS and
    E1: cS.j = x by C, FUNCT_1:def 5;
        reconsider j as Nat by D1, FINSEQ_3:25; f.j =b.x by D1, E1, FUNCT_1:23;
        then f.j = 0 by C1, POLYNOM1:def 7; then j in dd by D1, B, E;
     hence dd is non empty;
    end;
 L: dd c= dom f proof let x be set; assume x in dd; then
      ex j being Nat st x = j & j in dom f & f.j = 0;
     hence thesis;
    end; then
    reconsider dd as finite non empty set by M, FINSET_1:13;
    rng canFS(dd) = dd & dd c= NAT by CFS1, L, E, XBOOLE_1:1; then
    reconsider cdd = canFS(dd) as FinSequence of NAT by FINSEQ_1:def 4;
    set cdi = cdd";
    reconsider cdi as Function of dd, Seg card dd by CFS3;
    reconsider cadd = card dd as non empty Nat by GRAPH_5:5;
 V: Seg cadd <> {} & Seg card dd c= NAT; then
    reconsider cdi as Function of dd, NAT by FUNCT_2:9;
     set cSr = cS | (dom f \ dd);
 Ub: cSr is one-to-one by Ca, FUNCT_1:84;
     dom f \ dd c= dom f by XBOOLE_1:36; then
     (dom f \ dd) /\ dom f = dom f \ dd by XBOOLE_1:28; then
 Uc: dom cSr = (dom f \ dd) by B, E, FUNCT_1:68;
     now let y be set;
      hereby assume y in rng cSr; then consider x being set such that
      A1: x in dom cSr and
      B1: y = cSr.x by FUNCT_1:def 5;
      C1: x in dom cS & x in dom f \ dd by A1, RELAT_1:86; then
          reconsider j = x as Nat by FINSEQ_3:25;
      D1: cSr.x = cS.x by A1, FUNCT_1:70;
          not j in dd by C1, XBOOLE_0:def 4; then
          f.j <> 0 by C1, B, E; then
          b.(cS.j) <> 0 by C1, FUNCT_1:23;
       hence y in support b by B1, D1, POLYNOM1:def 7;
      end;
      assume A1: y in support b; then y in S by A; then
        consider x being set such that
      B1: x in dom cS and
      C1: y = cS.x by C, FUNCT_1:def 5;
          now assume x in dd; then consider j being Nat such that
          A2: j = x and
          B2: j in dom f and
          C2: f.j = 0;
          0 = b.(cS.j) by C2, B2, B, E, FUNCT_1:23;
           hence contradiction by A1, A2, C1, POLYNOM1:def 7;
          end; then x in dom f \ dd by B1, B, E, XBOOLE_0:def 4;      
      hence y in rng cSr by B1, C1, FUNCT_1:73;
     end; then
     rng cSr = support b by TARSKI:2; then
     support b, dom f \dd are_equipotent by Ub, Uc, WELLORD2:def 4; then
 Ua: card support b = card (dom f \ dd) by CARD_1:81;  
     card (dom f \ dd) = card dom f - card dd by L, CARD_2:63; then
     card (dom f \ dd) = card S - card dd by E, FINSEQ_1:78; then
     card support b + card dd = card S - card dd + card dd by Ua; then
     card support b + card dd = card S by XCMPLX_1:27; then     
 U: card dd = d by J, XCMPLX_1:2;
    len cdd = card dd by LCFS; then
 Va: dom cdd = Seg d by U, FINSEQ_1:def 3;
 Vb: rng cdd = dd by CFS1;
 Vc: dom cdi = dd by FUNCT_2:def 1;
 Vd: cdd is one-to-one by CFS0; then
 Ve: cdi is one-to-one by FUNCT_1:62;
 Vf: rng cdi = Seg d by Vd, Va, FUNCT_1:55;
    deffunc Z(set) = cdi /. $1 + card support b;
    consider z being Function such that
 R: dom z = dd and
 S: for x being set st x in dd holds z.x = Z(x) from Lambda;
 Sa: rng z c= Seg card S proof let y be set; assume y in rng z; then
         consider x being set such that
     A1: x in dom z and
     B1: y = z.x by FUNCT_1:def 5;
     C1: y = cdi/.x + card support b by A1, R, S, B1;
     E1: cdi/.x = cdi.x by A1, R, Vc, FINSEQ_4:def 4;
         cdi.x in Seg d by Vf, A1, R, Vc, FUNCT_1:12; then
         1 <= cdi/.x & cdi/.x <= d by E1, FINSEQ_1:3; then
         1 <= cdi/.x + card support b &
         cdi/.x + card support b <= d + card support b by NAT_1:37, AXIOMS:24;
         then cdi/.x + card support b in Seg card S by J, FINSEQ_1:3;
       hence thesis by C1;
     end;
    set p = cs"*cS +* z;
 Tc: dom p = dom (cs"*cS) \/ dom z by FUNCT_4:def 1;
 Tb: now assume dom (cs"*cS) /\ dom z <> {}; then
         consider x being set such that
     A1: x in dom (cs"*cS) /\ dom z by XBOOLE_0:def 1;
     B1: x in dom (cs"*cS) & x in dom z by A1, XBOOLE_0:def 3;
         then consider j being Nat such that
     C1: j = x and j in dom f and
     E1: f.j = 0 by R;
     H1: dom (cs") = support b by Hc, Ga, FUNCT_1:55;
         j in dom cS by B1, C1, FUNCT_1:21; then
         f.j = b.(cS.j) by FUNCT_1:23; then
         not cS.j in support b by E1, POLYNOM1:def 7; 
      hence contradiction by C1, B1, H1, FUNCT_1:21;
     end;
     now let x be set;
      hereby assume S1: x in dom (cs"*cS) \/ dom z;
       per cases by S1, XBOOLE_0:def 2;
       suppose x in dom (cs"*cS); then x in dom cS by FUNCT_1:21;
        hence x in dom F by Ka, B;
       suppose x in dom z;
        hence x in dom F by L, Ka, E, R;
      end;
      assume
     A1: x in dom F; then reconsider i = x as Nat by FINSEQ_3:25;
      per cases;
      suppose f.x = 0; then i in dom z by R, A1, Ka, E;
       hence x in dom (cs"*cS) \/ dom z by XBOOLE_0:def 2;
      suppose S1: f.x <> 0;
      B1: i in dom cS by A1, Ka, B; then
      C1: f.i = b.(cS.i) by FUNCT_1:23;
          cS.i in support b by S1, C1, POLYNOM1:def 7; then
          cS.i in rng cs by Hc; then cS.i in dom (cs") by Ga, FUNCT_1:55;
          then i in dom (cs"*cS) by B1, FUNCT_1:21;
       hence x in dom (cs"*cS) \/ dom z by XBOOLE_0:def 2;
     end; then
 Ta: dom (cs"*cS) \/ dom z = dom F by TARSKI:2; then
 T: dom p = dom F by FUNCT_4:def 1;
    now let x be set such that
    A1: x in dom F;
     per cases by A1, Ta, XBOOLE_0:def 2;
     suppose S1: x in dom (cs"*cS);
          not x in dom z by S1, Tb, XBOOLE_0:def 3; then
      K1: p.x = (cs"*cS).x by FUNCT_4:12;
          (cs"*cS).x in rng (cs"*cS) by S1, FUNCT_1:12; then
          (cs"*cS).x in rng (cs") by FUNCT_1:25; then
          (cs"*cS).x in dom cs by Ga, FUNCT_1:55; then
      L1: (cs"*cS).x in Seg card support b by Hb;
          Seg card support b c= Seg card S by I, FINSEQ_1:7;
      hence p.x in dom F by K1, L1, Ka;
     suppose S1: x in dom z; then
     B1: p.x = z.x by FUNCT_4:14;         z.x in rng z by S1, FUNCT_1:12;
      hence p.x in dom F by B1, Ka, Sa;     
    end; then
    reconsider p as Function of dom F, dom F by T, FUNCT_2:5;
 Na: p is one-to-one proof let a, c be set such that
     A1: a in dom p and
     B1: c in dom p and
     C1: p.a = p.c;
     D1: (a in dom (cs"*cS) or a in dom z) by A1, Tc, XBOOLE_0:def 2;
     E1: (c in dom (cs"*cS) or c in dom z) by B1, Tc, XBOOLE_0:def 2;
      per cases by D1, E1;
      suppose S1: a in dom (cs"*cS) & c in dom (cs"*cS);
          not a in dom z by S1, Tb, XBOOLE_0:def 3; then             
      K1: p.a = (cs"*cS).a by FUNCT_4:12 .= cs".(cS.a) by S1, FUNCT_1:22;
          not c in dom z by S1, Tb, XBOOLE_0:def 3; then             
      L1: p.c = (cs"*cS).c by FUNCT_4:12 .= cs".(cS.c) by S1, FUNCT_1:22;
      M1: cs.(cs".(cS.a)) = cs.(cs".(cS.c)) by C1, K1, L1;
          cS.a in dom (cs") by S1, FUNCT_1:21; then
          cS.a in rng cs by Ga, FUNCT_1:55; then
      N1: cs.(cs".(cS.a)) = cS.a by Ga, FUNCT_1:57;
          cS.c in dom (cs") by S1, FUNCT_1:21; then
          cS.c in rng cs by Ga, FUNCT_1:55; then
          cs.(cs".(cS.c)) = cS.c by Ga, FUNCT_1:57; then
      O1: cS".(cS.a) = cS".(cS.c) by N1, M1;
          a in dom cS by S1, FUNCT_1:21; then
      P1: cS".(cS.a) = a by Ca, FUNCT_1:56;
          c in dom cS by S1, FUNCT_1:21; then      
          cS".(cS.c) = c by Ca, FUNCT_1:56;
        hence a = c by O1, P1;
      suppose S1: a in dom (cs"*cS) & c in dom z;
      K1: p.c = z.c by S1, FUNCT_4:14 .= cdi /. c + card support b by S1, R, S;
          not a in dom z by S1, Tb, XBOOLE_0:def 3; then             
      L1: p.a = (cs"*cS).a by FUNCT_4:12 .= cs".(cS.a) by S1, FUNCT_1:22;
          cS.a in dom (cs") by S1, FUNCT_1:21; then
          cs".(cS.a) in rng (cs") by FUNCT_1:12; then
      M1: cs".(cS.a) in dom cs by Ga, FUNCT_1:55; then
          reconsider ccc = cs".(cS.a) as Nat by FINSEQ_3:25;
          cdi /. c + card support b <= 0+card support b
              by C1, K1, L1, M1, Hb, FINSEQ_1:3; then
      N1: cdi /. c <= 0 by REAL_1:53;          cdi /. c >= 0 by NAT_1:18; then
      P1: cdi /. c = 0 by N1; then
      O1: cdi.c = 0 by S1, R, Vc, FINSEQ_4:def 4; 
          cdi.c in rng cdi by S1, R, Vc, FUNCT_1:12; then
          1 <= cdi/.c by O1, Vf, FINSEQ_1:3;
       hence a = c by P1;
      suppose S1: a in dom z & c in dom (cs"*cS);
      K1: p.a = z.a by S1, FUNCT_4:14 .= cdi /. a + card support b by S1, R, S;
          not c in dom z by S1, Tb, XBOOLE_0:def 3; then             
      L1: p.c = (cs"*cS).c by FUNCT_4:12 .= cs".(cS.c) by S1, FUNCT_1:22;
          cS.c in dom (cs") by S1, FUNCT_1:21; then
          cs".(cS.c) in rng (cs") by FUNCT_1:12; then
      M1: cs".(cS.c) in dom cs by Ga, FUNCT_1:55; then
          reconsider ccc = cs".(cS.c) as Nat by FINSEQ_3:25;
          cdi /. a + card support b <= 0+card support b
              by C1, K1, L1, M1, Hb, FINSEQ_1:3; then
      N1: cdi /. a <= 0 by REAL_1:53;          cdi /. a >= 0 by NAT_1:18; then
      P1: cdi /. a = 0 by N1; then
      O1: cdi.a = 0 by S1, R, Vc, FINSEQ_4:def 4; 
          cdi.a in rng cdi by S1, R, Vc, FUNCT_1:12; then
          1 <= cdi/.a by O1, Vf, FINSEQ_1:3;
       hence a = c by P1;
      suppose S1: a in dom z & c in dom z;
      K1: p.a = z.a by S1, FUNCT_4:14 .= cdi /. a + card support b by S1, R, S;
      L1: p.c = z.c by S1, FUNCT_4:14 .= cdi /. c + card support b by S1, R, S;
      O1: cdi /. a = cdi /. c by K1, L1, C1, XCMPLX_1:2;
          cdi /. a = cdi . a & cdi /. c = cdi . c by S1,Vc,R,FINSEQ_4:def 4;
       hence a = c by Ve, S1, Vc, R, O1, FUNCT_1:def 8;
     end;
    now let x be set;
     hereby assume x in rng p; then consider a being set such that
     A1: a in dom p and
     B1: x = p.a by FUNCT_1:def 5;
      per cases by A1, FUNCT_4:13;
      suppose S1: a in dom (cs"*cS);
          not a in dom z by S1, Tb, XBOOLE_0:def 3; then
     C1: p.a = (cs"*cS).a by FUNCT_4:12 .= cs".(cS.a) by S1, FUNCT_1:22;
         cS.a in dom (cs") by S1, FUNCT_1:21; then
         cs".(cS.a) in rng (cs") by FUNCT_1:12; then
     D1: cs".(cS.a) in dom cs by Ga, FUNCT_1:55;
         dom cs c= dom F by I, Ka, Hb, FINSEQ_1:7;
       hence x in dom F by D1, C1, B1;
      suppose S1: a in dom z; then
      C1: z.a in rng z by FUNCT_1:12;        p.a = z.a by S1, FUNCT_4:14;
       hence x in dom F by B1, Ka, Sa, C1;
     end;
     assume A1: x in dom F; then reconsider j = x as Nat by FINSEQ_3:25;
     per cases by A1, FINSEQ_1:38;
     suppose j in dom gr; then
     B1: j in dom cs by Hb, Hd; then
     H1: cs.j in support b by Hc, FUNCT_1:12; then
     F1: cs.j in S by A; then
     E1: cS".(cs.j) in Seg card S by B, Ca, C, FUNCT_1:54; then
     C1: cS".(cs.j) in dom p by T, Ka;
     G1: cs.j in dom (cS*cS") by Ca, C, F1, FUNCT_1:59;
         now assume
         A2: cS".(cs.j) in dom z;
             (b*cS).(cS".(cs.j)) = b.(cS.(cS".(cs.j))) by E1, B, FUNCT_1:23
             .= b.(cs.j) by F1, C, Ca, FUNCT_1:57; then
         B2: f.(cS".(cs.j)) <> 0 by H1, POLYNOM1:def 7;
             ex k being Nat st k = cS".(cs.j) & k in dom f & f.k = 0 by A2, R;
          hence contradiction by B2;
         end; then p.(cS".(cs.j)) = (cs"*cS).(cS".(cs.j)) by FUNCT_4:12
         .= cs".(cS.(cS".(cs.j))) by E1, B, FUNCT_1:23
         .= cs".((cS*cS").(cs.j)) by G1, FUNCT_1:22
         .= cs".(cs.j) by F1, C, Ca, FUNCT_1:57 .= (cs"*cs).j by B1, FUNCT_1:23
         .= j by B1, Ga, FUNCT_1:56;
      hence x in rng p by C1, FUNCT_1:12;
     suppose ex n being Nat st n in dom h & j=len gr + n; then
       consider n being Nat such that
     A1: n in dom h and
     B1: j = len gr + n;
     D1: cdd.n in dd by A1, Va, Vb, Kc, FUNCT_1:12; then
         cdd.n in dom f by L; then
     C1: cdd.n in dom p by Ka, E, T;
         p.(cdd.n) = z.(cdd.n) by D1, R, FUNCT_4:14
      .= cdi /. (cdd.n) + card support b by D1, S
      .= cdi.(cdd.n) + card support b by D1, Vc, FINSEQ_4:def 4
      .= n + card support b by A1, Va, Kc, Vd, FUNCT_1:56 .= j by B1, Ha;
      hence x in rng p by C1, FUNCT_1:12;
    end; then
 Nc: rng p = dom F by TARSKI:2; then p is onto by FUNCT_2:def 3; then
 N: p is Permutation of dom F by Na, FUNCT_2:def 4;
 Pc: dom (F*p) = dom F by T, Nc, RELAT_1:46; then
 Pa: dom f = dom (F*p) by Ka, E;
    now let x be set; assume
    A1: x in dom f;
    per cases;
    suppose S1: f.x = 0;
       reconsider j = x as Nat by A1, FINSEQ_3:25;
    B1: j in dom z by A1, S1, R; then
    C1: p.x = z.x by FUNCT_4:14 .= cdi /. x + card support b by B1, S, R;
        p.x in dom F by T, A1, Pc, Pa, Nc, FUNCT_1:12; then
        reconsider px = p.x as Nat by FINSEQ_3:25;
        dom cdi = dd by FUNCT_2:def 1; then
    E1: cdi /. x = cdi.x by B1, R, FINSEQ_4:def 4;
        cdi.x in Seg card dd by V, B1, R, FUNCT_2:7; then
    D1: cdi /. x in dom h by E1, Kc, U;
        reconsider cdix = cdi /. x as Nat;
     thus f.x = h.(cdix) by Kc, S1, D1, FINSEQ_2:70
       .= F.px by C1, Ha, D1, FINSEQ_1:def 7 .= (F*p).x by A1, Pa, FUNCT_1:22;
    suppose S1: f.x <> 0; 
    B1: now assume x in dd; then ex j being Nat st j=x & j in dom f & f.j = 0;
         hence contradiction by S1;
        end;        f.x = b.(cS.x) by A1, FUNCT_1:22; then
        cS.x in support b by S1, POLYNOM1:def 7; then
    C1: cS.x in rng cs by CFS1; then
    D1: cs".(cS.x) in dom cs by Ga, FUNCT_1:54;
    E1: cS.x = cs.(cs".(cS.x)) by C1, Ga, FUNCT_1:54;
    F1: p.x = (cs"*cS).x by R, B1, FUNCT_4:12
           .= cs".(cS.x) by A1, B, E, FUNCT_1:23; then
    G1: p.x in dom g by D1, Hd, Hb; then
        reconsider px = p.x as Nat by FINSEQ_3:25;
     thus f.x = b.(cS.x) by A1, FUNCT_1:22
       .= b.(cs.px) by E1, F1 .= g.(px) by H, D1, F1, FUNCT_1:23
       .= F.(px) by G1, FINSEQ_1:def 7 .= (F*p).x by A1, Pa, FUNCT_1:22;
    end; then
 P: f = F*p by Pa, FUNCT_1:9;
 R: addreal is commutative associative & addreal has_a_unity by RVSUM_1:5,6,7;
 O: Sum F = addreal $$ F by RVSUM_1:def 10
         .= addreal $$ fr by P, R, N, FINSOP_1:8 .= Sum f by RVSUM_1:def 10;
    Sum h = 0 by RVSUM_1:111;
    then Sum gr = Sum gr + Sum h .= Sum F by RVSUM_1:105;
  hence degree b = Sum f by O, G;
 suppose card support b = card S; then support b = S by A, TRIANG_1:3;
  hence degree b = Sum f by G, H;
end;

theorem BAGDEG2: :: BAGDEG2:
for A being set, b, b1, b2 being bag of A
 st b = b1 + b2 holds degree b = degree b1 + degree b2
proof let A be set, b, b1, b2 be bag of A; assume
A: b = b1 + b2;
   consider f being FinSequence of NAT such that
B: degree b = Sum f and
C: f = b*canFS(support b) by LBAGDEG;   set S = support b;
Z: dom b = A & dom b1 = A & dom b2 = A by PBOOLE:def 3;
   S c= dom b by POLYNOM1:41; then reconsider S as finite Subset of A by Z;
D: S = support b1 \/ support b2 by A, POLYNOM1:42;
   then support b1 c= S by XBOOLE_1:7; then
   consider f1r being FinSequence of NAT such that
I: f1r = b1*canFS(S) and
J: degree b1 = Sum f1r by BAGDEG2c;    support b2 c= S by D, XBOOLE_1:7; then
   consider f2r being FinSequence of NAT such that
K: f2r = b2*canFS(S) and
L: degree b2 = Sum f2r by BAGDEG2c;
   rng f c= NAT & rng f1r c= NAT & rng f2r c= NAT by FINSEQ_1:def 4; then
   rng f c= REAL & rng f1r c= REAL & rng f2r c= REAL by XBOOLE_1:1; then
   reconsider f,f1r,f2r as FinSequence of REAL by FINSEQ_1:def 4;
   set cS = canFS S; rng cS = S by CFS1; then
O: dom f = dom cS & dom f1r = dom cS & dom f2r = dom cS
     by Z, C, I, K, RELAT_1:46; then
N: len f1r = len f2r & len f1r = len f by FINSEQ_3:31;
   now let k be Nat such that
   A1: k in dom f1r;
   B1: f1r/.k = f1r.k by A1, FINSEQ_4:def 4 .= b1.(cS.k) by A1, I, FUNCT_1:22;
   C1: f2r/.k = f2r.k by A1, O, FINSEQ_4:def 4
       .= b2.(cS.k) by A1, K, O, FUNCT_1:22;
       f.k = b.(cS.k) by A1, C, O, FUNCT_1:22;
    hence f.k = f1r/.k + f2r/.k by B1, C1, A, POLYNOM1:def 5;
   end; then
   Sum f = (Sum f1r) + Sum f2r by N, INTEGRA1:23;
 hence degree b = degree b1 + degree b2 by B, J, L;
end;

theorem Permprod: :: GROUP_4:18 but about a different Product
for L being associative commutative unital (non empty HGrStr),
    f, g being FinSequence of L, p being Permutation of dom f
  st g = f * p holds Product(g) = Product(f)
proof let L be associative commutative unital (non empty HGrStr),
          f, g be FinSequence of L, p be Permutation of dom f such that
A: g = f * p;   set mL = (the mult of L);
B: mL is commutative by MONOID_0:def 11;
C: mL is associative by GROUP_1:31;
D: mL has_a_unity by GROUP_1:34;
 thus Product(g) = (the mult of L) $$ g by FVSUM_1:def 9
    .= (the mult of L) $$ f by A, B, C, D, FINSOP_1:8
    .= Product(f) by FVSUM_1:def 9;
end;

begin :: More on polynomials

definition
  let L be non empty ZeroStr, p be Polynomial of L;
  attr p is non-zero means                                       :LNZ:
   p <> 0_. L;
end;

theorem lenNZ: :: lenNZ
for L being non empty ZeroStr, p being Polynomial of L
 holds p is non-zero iff len p > 0
proof let L be non empty ZeroStr, p be Polynomial of L;
 hereby assume p is non-zero; then p <> 0_. L by LNZ;
   then len p <> 0 by POLYNOM4:8; 
  hence len p > 0 by NAT_1:19;
 end;
 assume len p > 0; then p <> 0_. L by POLYNOM4:6;
 hence p is non-zero by LNZ;
end;


definition
  let L be non trivial (non empty ZeroStr);
  cluster non-zero Polynomial of L;
  existence proof
   consider a being Element of (the carrier of L)\{0.L};
   the carrier of L is non trivial by REALSET1:def 13;
   then (the carrier of L)\{0.L} is non empty by REALSET1:32;
   then A1: a in the carrier of L & not(a in {0.L}) by XBOOLE_0:def 4;
   then reconsider a as Element of L;
   take p = <%a%>;
   p.0 = a & (0_. L).0 = 0.L by POLYNOM3:28, POLYNOM5:33; then
   p <> 0_. L by A1, TARSKI:def 1;
 hence thesis by LNZ;
 end;
end;

definition
  let L be non degenerated non empty multLoopStr_0, x be Element of L;
  cluster <%x, 1_ L%> -> non-zero;
  correctness proof 0.L <> 1_ L by VECTSP_1:def 21;
   then len <%x, 1_ L%> = 2 by POLYNOM5:41;
   hence thesis by lenNZ;
  end;
end;

theorem LC1:
for L being non empty ZeroStr, p being Polynomial of L
 st len p > 0 holds p.(len p -'1) <> 0.L
proof let L be non empty ZeroStr, p be Polynomial of L; assume
   len p > 0; then consider k being Nat such that
B: len p = k+1 by NAT_1:22;
   len p = (len p -'1)+1 by B, BINARITH:39; 
  hence p.(len p -'1) <> 0.L by ALGSEQ_1:25;
end;

theorem plen1: :: plen1:
for L being non empty ZeroStr, p being AlgSequence of L
 st len p = 1 holds p = <%p.0%> & p.0 <> 0.L
proof let L be non empty ZeroStr, p being AlgSequence of L such that
A: len p = 1;
 thus B: p=<%p.0%> by A, ALGSEQ_1:def 6;    p <> <%0.L%> by A, ALGSEQ_1:31;
 hence p.0 <> 0.L by B;
end;

theorem P4Th5: :: P4Th5: from POLYNOM4:5 right-distributive 
for L be add-associative right_zeroed right_complementable
         right-distributive (non empty doubleLoopStr),
    p be Polynomial of L holds p*'(0_.(L)) = 0_.(L)
proof let L be add-associative right_zeroed right_complementable
            right-distributive (non empty doubleLoopStr), p be Polynomial of L;
  now let i be Nat;  consider r be FinSequence of L such that
      len r = i+1 and
  A1: (p*'(0_.(L))).i = Sum r and
  A2: for k be Nat st k in dom r holds r.k = p.(k-'1) * (0_. L).(i+1-'k)
                                                         by POLYNOM3:def 11;
     now let k be Nat; assume k in dom r;
      hence r.k = p.(k-'1) * (0_. L).(i+1-'k) by A2
         .= p.(k-'1) * 0.L by POLYNOM3:28 .= 0.L by VECTSP_1:36;
     end;
     hence (p*'(0_.(L))).i = 0.L by A1,POLYNOM3:1 .= (0_.(L)).i by POLYNOM3:28;
  end;
 hence thesis by FUNCT_2:113;
end;

definition
  cluster algebraic-closed add-associative right_zeroed right_complementable
     Abelian commutative associative distributive domRing-like
     non degenerated (well-unital (non empty doubleLoopStr));
   existence proof take F_Complex; thus thesis; end;
end;

theorem pintdom: :: pintdom:
for L being add-associative right_zeroed right_complementable distributive
            domRing-like (non empty doubleLoopStr),
    p, q being Polynomial of L
 st p*'q = 0_. L holds p = 0_. L or q = 0_. L
proof let L be add-associative right_zeroed right_complementable distributive
                           domRing-like (non empty doubleLoopStr),
          p, q being Polynomial of L such that
A: p*'q = 0_. L and
B: p <> 0_. L and
C: q <> 0_. L;
Ba: len p <> 0 by B, POLYNOM4:8; then consider lp1 being Nat such that
D: len p = lp1+1 by NAT_1:22; len q <> 0 by C, POLYNOM4:8;
   then consider lq1 being Nat such that
E: len q = lq1+1 by NAT_1:22;
F: p.lp1 <> 0.L & q.lq1 <> 0.L by D, E, ALGSEQ_1:25;
   set lpq = lp1 + lq1;
   consider r being FinSequence of L such that
G: len r = lpq+1 and
H: (p*'q).lpq = Sum r and
I: for k be Nat st k in dom r holds r.k=p.(k-'1)*q.(lpq+1-'k)
           by POLYNOM3:def 11;   len p <= lp1+1+lq1 by D, NAT_1:37; then
   len p <= lp1+(1+lq1) by XCMPLX_1:1; then
N: len p <= lp1+lq1+1 by XCMPLX_1:1;   0 < len p by Ba, NAT_1:19; then
M: 0+1 <= len p by NAT_1:38;
J: len p in dom r by M, N, G, FINSEQ_3:27;
K: lpq+1-'len p = lq1+(lp1+1)-'len p by XCMPLX_1:1 .= lq1 by D, BINARITH:39;
   now let k be Nat such that
   A1: k in dom r and
   B1: k <> len p;
   C1: r.k = p.(k-'1) * q.(lpq+1-'k) by A1, I;
    per cases by B1, REAL_1:def 5;
    suppose k < len p; then consider d being Nat such that
   D1: len p = k+d & 1 <= d by FSM_1:1;
       lpq+1 = lq1 +len p by D, XCMPLX_1:1; then
   E1: lpq+1-'k = lq1+d+k-'k by D1, XCMPLX_1:1 .= lq1+d by BINARITH:39;
       len q <= lq1+d by D1, E, AXIOMS:24; 
      hence r.k = p.(k-'1)*0.L by C1, E1, ALGSEQ_1:22 .= 0.L by VECTSP_1:36;
    suppose k > len p; then k >= len p + 1 by NAT_1:38; then
        k-'1 >= len p + 1-'1 by JORDAN3:5; then k-'1 >= len p by BINARITH:39;
      hence r.k = 0.L * q.(lpq+1-'k) by C1, ALGSEQ_1:22 .= 0.L by VECTSP_1:39;
   end;
   then Sum r = r.(len p) by J, MATRIX_3:14
   .= p.(len p -'1)*q.(lpq+1-'len p) by J,I.= p.lp1 * q.lq1 by K,D,BINARITH:39;
   then Sum r <> 0.L by F, VECTSP_2:def 5;
 hence contradiction by A, H, POLYNOM3:28;
end;

definition
  let L be add-associative right_zeroed right_complementable distributive
           domRing-like (non empty doubleLoopStr);
  cluster Polynom-Ring L -> domRing-like;
  correctness proof   set PRL = Polynom-Ring L;  
    let x, y be Element of PRL;
    reconsider xp = x, yp = y as Polynomial of L by POLYNOM3:def 12;
  Z: 0_. L = 0.PRL  by POLYNOM3:def 12; 
    assume x*y = 0.PRL; then xp*'yp = 0_. L by Z, POLYNOM3:def 12; 
   hence x = 0.PRL or y = 0.PRL by Z, pintdom;
  end;
end;

definition
  let L be domRing, p, q be non-zero Polynomial of L;
  cluster p*'q -> non-zero;
  correctness proof p <> 0_. L & q <> 0_. L by LNZ;
   then p*'q <> 0_. L by pintdom;
   hence thesis by LNZ;
  end;
end;

theorem :: pcomring0:
for L being non degenerated comRing, p, q being Polynomial of L
 holds Roots p \/ Roots q c= Roots (p*'q) 
proof let L be non degenerated comRing, p, q being Polynomial of L;
  let x be set;
  assume A: x in Roots p \/ Roots q;
  per cases by A, XBOOLE_0:def 2;
  suppose B: x in Roots p; then reconsider a = x as Element of L;
    a is_a_root_of p by B, POLYNOM5:def 9; then
    eval(p,a) = 0.L by POLYNOM5:def 6; then
    eval(p,a) * eval(q,a) = 0.L by VECTSP_1:39; then
    eval(p*'q,a) = 0.L by POLYNOM4:27; then
    a is_a_root_of p*'q by POLYNOM5:def 6;
   hence x in Roots (p*'q) by POLYNOM5:def 9;
  suppose B: x in Roots q; then reconsider a = x as Element of L;
    a is_a_root_of q by B, POLYNOM5:def 9; then
    eval(q,a) = 0.L by POLYNOM5:def 6; then
    eval(p,a) * eval(q,a) = 0.L by VECTSP_1:36; then
    eval(p*'q,a) = 0.L by POLYNOM4:27; then
    a is_a_root_of p*'q by POLYNOM5:def 6;
   hence x in Roots (p*'q) by POLYNOM5:def 9;
end;

theorem pdomring0: :: pdomring0:
for L being domRing, p, q being Polynomial of L
 holds Roots (p*'q) = Roots p \/ Roots q
proof let L be domRing, p, q being Polynomial of L;
 now let x be set;
  hereby assume
  A: x in Roots (p*'q); then  reconsider a = x as Element of L;
     a is_a_root_of p*'q by A, POLYNOM5:def 9; then
     eval(p*'q,a) = 0.L by POLYNOM5:def 6; then
     eval(p,a) * eval(q,a) = 0.L by POLYNOM4:27; then
  B: eval(p,a) = 0.L or eval(q,a) = 0.L by VECTSP_2:def 5;
   per cases by B;
   suppose eval(p,a) = 0.L; then a is_a_root_of p by POLYNOM5:def 6; then
     a in Roots p by POLYNOM5:def 9;
    hence x in Roots p \/ Roots q by XBOOLE_0:def 2;
   suppose eval(q,a) = 0.L; then a is_a_root_of q by POLYNOM5:def 6; then
     a in Roots q by POLYNOM5:def 9;
    hence x in Roots p \/ Roots q by XBOOLE_0:def 2;
  end;
  assume A: x in Roots p \/ Roots q;
  per cases by A, XBOOLE_0:def 2;
  suppose B: x in Roots p; then reconsider a = x as Element of L;
    a is_a_root_of p by B, POLYNOM5:def 9; then
    eval(p,a) = 0.L by POLYNOM5:def 6; then
    eval(p,a) * eval(q,a) = 0.L by VECTSP_1:39; then
    eval(p*'q,a) = 0.L by POLYNOM4:27; then
    a is_a_root_of p*'q by POLYNOM5:def 6;
   hence x in Roots (p*'q) by POLYNOM5:def 9;
  suppose B: x in Roots q; then reconsider a = x as Element of L;
    a is_a_root_of q by B, POLYNOM5:def 9; then
    eval(q,a) = 0.L by POLYNOM5:def 6; then
    eval(p,a) * eval(q,a) = 0.L by VECTSP_1:36; then
    eval(p*'q,a) = 0.L by POLYNOM4:27; then
    a is_a_root_of p*'q by POLYNOM5:def 6;
   hence x in Roots (p*'q) by POLYNOM5:def 9;
 end;
 hence Roots (p*'q) = Roots p \/ Roots q by TARSKI:2;
end;

theorem puminus: :: puminus:
for L being add-associative right_zeroed right_complementable distributive
            (non empty doubleLoopStr),
    p being (Polynomial of L), pc being (Element of Polynom-Ring L)
 st p = pc holds -p = -pc
proof let L be add-associative right_zeroed right_complementable distributive
               (non empty doubleLoopStr),
   p be (Polynomial of L), pc be (Element of Polynom-Ring L) such that
A: p = pc;
   set PRL = Polynom-Ring L;
   reconsider mpc = -p as Element of PRL by POLYNOM3:def 12;
   p+-p = p-p by POLYNOM3:def 8 .= 0_. L by POLYNOM3:30; then
   pc + mpc = 0_. L by A, POLYNOM3:def 12 .= 0.PRL by POLYNOM3:def 12; 
 hence -p = -pc by RLVECT_1:def 10;
end;

theorem pminus: :: pminus:
for L being add-associative right_zeroed right_complementable distributive
            (non empty doubleLoopStr),
    p, q being (Polynomial of L), pc, qc being (Element of Polynom-Ring L)
 st p= pc & q = qc holds p-q = pc-qc
proof let L be add-associative right_zeroed right_complementable distributive
               (non empty doubleLoopStr),
    p,q be (Polynomial of L), pc,qc be (Element of Polynom-Ring L) such that
A: p = pc and
B: q = qc;
C: -q = -qc by B, puminus;
 thus p-q = p+-q by POLYNOM3:def 8 .= pc+-qc by A, C,POLYNOM3:def 12
   .= pc-qc by RLVECT_1:def 11;
end;

theorem distrminus: :: distrminus:
for L being Abelian add-associative right_zeroed right_complementable
            distributive (non empty doubleLoopStr),
    p, q, r being (Polynomial of L)
 holds  p*'q-p*'r = p*'(q-r)
proof let L be Abelian add-associative right_zeroed right_complementable
               distributive (non empty doubleLoopStr),
    p, q, r be (Polynomial of L);
   set PRL = Polynom-Ring L;
   reconsider pc = p, qc = q, rc = r as Element of PRL by POLYNOM3:def 12;
A: p*'q = pc*qc by POLYNOM3:def 12;
B: p*'r = pc*rc by POLYNOM3:def 12;
C: qc-rc = q-r by pminus;
 thus p*'q-p*'r = pc*qc - pc*rc by A, B, pminus
       .= pc*(qc-rc) by VECTSP_1:43 .= p*'(q-r) by C, POLYNOM3:def 12;
end;

theorem minus0: :: minus0:
for L being add-associative right_zeroed right_complementable distributive
            (non empty doubleLoopStr),
    p, q being (Polynomial of L)
 st p-q = 0_. L holds p = q
proof let L be add-associative right_zeroed right_complementable distributive
            (non empty doubleLoopStr),
          q, r be (Polynomial of L);
   set PRL = Polynom-Ring L;
   reconsider qc = q, rc = r as Element of PRL by POLYNOM3:def 12;
Z: 0_. L = 0.PRL  by POLYNOM3:def 12; 
   assume  q-r = 0_. L; then qc-rc = 0.PRL by Z,pminus; then
   qc=rc by VECTSP_1:84;
 hence q = r;
end; 

theorem pcanc0: :: pcanc0:
for L being Abelian add-associative right_zeroed right_complementable
            distributive domRing-like (non empty doubleLoopStr),
    p, q, r being Polynomial of L
 st p <> 0_. L & p*'q = p*'r holds q = r
proof let L be Abelian add-associative right_zeroed right_complementable
               distributive domRing-like (non empty doubleLoopStr),
    p, q, r be Polynomial of L; assume 
A: p <> 0_. L;
   set PRL = Polynom-Ring L;
   reconsider pc = p, qc = q, rc = r as Element of PRL by POLYNOM3:def 12;
 assume p*'q = p*'r; then p*'q-p*'r = p*'r-p*'r; then
   p*'q-p*'r = 0_. L by POLYNOM3:30; then  p*'(q-r) = 0_. L by distrminus; then
   q-r = 0_. L by A, pintdom;
 hence q = r by minus0;
end; 
  
theorem pexp0: :: pexp0:
for L being domRing, n being Nat, p being Polynomial of L
 st p <> 0_. L holds p`^n <> 0_. L
proof let L be domRing, n be Nat, p be Polynomial of L; assume
A: p <> 0_. L;
   (1_. L).0 = 1_ L & (0_. L).0 = 0.L by POLYNOM3:28,31; then
B: 1_. L <> 0_. L by VECTSP_1:def 21;
    defpred P[Nat] means p`^$1 <> 0_. L;
    p`^0 = 1_. L by  POLYNOM5:16; then
BA: P[0] by B;
IS: for n being Nat st P[n] holds P[n+1] proof
       let n be Nat such that
    A1: P[n];        p`^(n+1) = (p`^n) *' p by POLYNOM5:20;
     hence P[n+1] by A1, A, pintdom;
    end;  for n being Nat holds P[n] from Ind(BA,IS);
  hence p`^n <> 0_. L;
end; 

theorem pexp1:  :: pexp1: 
for L being comRing, i, j being Nat, p being Polynomial of L
 holds (p`^i) *' (p`^j) = p `^(i+j)
proof let L be comRing, i, j being Nat, p be Polynomial of L;
 defpred P[Nat] means (p`^i) *' (p`^$1) = p `^(i+$1);
    (p`^i) *' (p`^0) = (p`^i) *' 1_. L by POLYNOM5:16
    .= (p`^(i+0)) by POLYNOM3:36; then
BA: P[0];
IS: for j being Nat st P[j] holds P[j+1] proof
     let j be Nat such that
    A: P[j];
       (p`^i) *' (p`^(j+1)) = (p`^i) *' ((p`^j) *' p) by POLYNOM5:20
       .= (p`^i) *' (p`^j) *' p by POLYNOM3:34 .= (p`^(i+j)) *' p by A
       .= p`^(i+j+1) by POLYNOM5:20   .= p`^(i+(j+1)) by XCMPLX_1:1;
     hence P[j+1];
    end; for j being Nat holds P[j] from Ind(BA,IS);
 hence (p`^i) *' (p`^j) = p `^(i+j);
end;

theorem poly1b: :: poly1b:
for L being non empty multLoopStr_0 holds 1_.(L) = <%1_ L%>
proof let L be non empty multLoopStr_0;
A: 1_.(L) = 0_.(L)+*(0,1_(L)) by POLYNOM3:def 10;
B: dom 0_.(L) = NAT by FUNCT_2:def 1;
  now let x be set; assume x in NAT; then reconsider n = x as Nat;
   per cases;
   suppose S1: x = 0;
    thus (1_.(L)).x = 1_(L) by S1, A, B, FUNCT_7:33
                   .= <%1_ L%>.x by S1, ALGSEQ_1:def 6;
   suppose S1: n <> 0; then n = 1 or n > 1 by neNat1; then
   A1: n >= 1;
    thus (1_.(L)).x = (0_.(L)).n by S1, A, FUNCT_7:34
      .= 0.L by POLYNOM3:28 .= <%1_ L%>.x by A1, POLYNOM5:33;    
  end;
 hence 1_.(L) = <%1_ L%> by FUNCT_2:18;
end; 

theorem  :: poly1a
for L being add-associative right_zeroed right_complementable right_unital
            right-distributive (non empty doubleLoopStr),
    p being Polynomial of L
 holds p*'<%1_ L%> = p
proof let L be add-associative right_zeroed right_complementable right_unital
               right-distributive      (non empty doubleLoopStr),
    p being Polynomial of L;
 thus p*'<%1_ L%> = p*'1_.(L) by poly1b .= p by POLYNOM3:36;
end;

theorem LM0:
for L being add-associative right_zeroed right_complementable distributive
                                                 (non empty doubleLoopStr),
    p, q being Polynomial of L
 st len p = 0 or len q = 0 holds len (p*'q) = 0  
proof let L be add-associative right_zeroed right_complementable distributive
               (non empty doubleLoopStr),
          p, q being Polynomial of L; assume
A: len p = 0 or len q = 0;
   per cases by A;
   suppose len p = 0; then p = 0_. L by POLYNOM4:8;
     then p*'q = 0_. L by POLYNOM4:5;
    hence len (p*'q) = 0 by POLYNOM4:6;
   suppose len q = 0; then q = 0_. L by POLYNOM4:8; then p*'q = 0_. L by P4Th5;
    hence len (p*'q) = 0 by POLYNOM4:6;
end;

theorem LM1: :: LM1
for L being add-associative right_zeroed right_complementable distributive
                                                 (non empty doubleLoopStr),
    p, q being Polynomial of L
 st p*'q is non-zero holds p is non-zero & q is non-zero
proof let L be add-associative right_zeroed right_complementable distributive
                                                 (non empty doubleLoopStr),
          p, q being Polynomial of L; assume that
A: p*'q is non-zero and
B: p is non non-zero or q is non non-zero;
B1: len p <= 0 or len q <= 0 by B, lenNZ;
   0 <= len p & 0 <= len q by NAT_1:18; then
   len p = 0 or len q = 0 by B1; then
   len (p*'q) = 0 by LM0;
 hence thesis by A, lenNZ;
end;

theorem :: LM1a
for L being add-associative right_zeroed right_complementable distributive
         commutative associative left_unital (non empty doubleLoopStr),
    p, q being Polynomial of L
 st p.(len p -'1) * q.(len q -'1) <> 0.L holds 0 < len (p*'q)
proof let L be add-associative right_zeroed right_complementable distributive
         commutative associative left_unital (non empty doubleLoopStr),
          p, q being Polynomial of L; assume 
Aa: p.(len p -'1) * q.(len q -'1) <> 0.L;
C: len (p*'q) = len p + len q -1 by Aa, POLYNOM4:13;
A1: now assume A2: len p <= 0; len p >= 0 by NAT_1:18;
       then len p = 0 by A2; then p = 0_. L by POLYNOM4:8;
       then p.(len p -'1) = 0.L by POLYNOM3:28; 
       hence contradiction by Aa, VECTSP_1:39;
      end;
  A2: now assume A2: len q <= 0; len q >= 0 by NAT_1:18;
       then len q = 0 by A2; then q = 0_. L by POLYNOM4:8;
       then q.(len q -'1) = 0.L by POLYNOM3:28; 
       hence contradiction by Aa,VECTSP_1:36;
      end;
  0+1 <= len p & 0+1 <= len q by A1, A2, NAT_1:38; then
  len p + len q >= 1+1 by REAL_1:55;
  then len p + len q -1 >= 1+1-1 by REAL_1:49;
  then len p + len q -1 >= 1 & 1 > 0;
 hence thesis by C;
end;

theorem LM2: :: LM2 
for L being add-associative right_zeroed right_complementable distributive
    commutative associative left_unital domRing-like (non empty doubleLoopStr),
    p, q being Polynomial of L
 st 1 < len p & 1 < len q holds len p < len (p*'q)
proof let L be add-associative right_zeroed right_complementable distributive
    commutative associative left_unital domRing-like (non empty doubleLoopStr),
          p, q be Polynomial of L such that
B: 1 < len p and
C: 1 < len q;
   0 < len p & 0 < len q by B, C, AXIOMS:22; then
   p.(len p -'1) <> 0.L & q.(len q -'1)<>0.L by LC1; then
   p.(len p -'1) * q.(len q -'1)<>0.L by VECTSP_2:def 5; then
E: len (p*'q) = len p + len q - 1 by POLYNOM4:13;
   len q - 1 > 1-1 by C, REAL_1:92; then len q - 1 > 0; then
   len p + (len q - 1) > 0+len p by REAL_1:67; then
   len p + (len q +- 1) > len p by XCMPLX_0:def 8; then
   len p + len q +- 1 > len p by XCMPLX_1:1; 
  hence len p < len (p*'q) by E, XCMPLX_0:def 8;
end;

theorem f2mpoly: :: f2mpoly:
for L being add-associative right_zeroed right_complementable
            left-distributive (non empty doubleLoopStr),
    a, b being Element of L, p being Polynomial of L
 holds (<%a, b%>*'p).0 = a*p.0 &
       for i being Nat holds (<%a, b%>*'p).(i+1) = a*p.(i+1)+b*p.i
proof let L be add-associative right_zeroed right_complementable
            left-distributive (non empty doubleLoopStr),
          a, b be Element of L, q be Polynomial of L;    set p = <%a, b%>;
    consider r being FinSequence of L such that
A:  len r = 0+1 and
B:  p*'q.0 = Sum r and
C:  for k be Nat st k in dom r holds r.k = p.(k-'1) * q.(0+1-'k)
      by POLYNOM3:def 11;
D:  1 in dom r by A, FINSEQ_3:27; then
    reconsider r1 = r.1 as Element of L by FINSEQ_2:13;
    r = <*r1*> by A, FINSEQ_1:57; then
    Sum r = r1 by RLVECT_1:61 .= p.(1-'1) * q.(0+1-'1) by C, D
 .= p.0 * q.(0+1-'1) by GOBOARD9:1 .= p.0 * q.0 by BINARITH:39;
 hence (<%a, b%>*'q).0 = a*q.0 by B, POLYNOM5:39;
 let i be Nat;
    consider r being FinSequence of L such that
A:  len r = (i+1)+1 and
B:  p*'q.(i+1) = Sum r and
C:  for k be Nat st k in dom r holds r.k = p.(k-'1) * q.((i+1)+1-'k)
      by POLYNOM3:def 11;
Aa: len r = i+(1+1) by A, XCMPLX_1:1 .= i+2;  0 <= i by NAT_1:18; then
D: 0+2 <= len r by Aa, AXIOMS:24;   1 <= len r by D, AXIOMS:22; then
E: 1 in dom r by FINSEQ_3:27;
F: 2 in dom r by D, FINSEQ_3:27;
G: r/.1 = r.1 by E, FINSEQ_4:def 4
   .= p.(1-'1) * q.((i+1)+1-'1) by E, C  .= p.0 * q.((i+1)+1-'1) by GOBOARD9:1
   .= p.0 * q.(i+1) by BINARITH:39  .= a*q.(i+1) by POLYNOM5:39;
H: r/.2 = r.2 by F, FINSEQ_4:def 4
   .= p.(2-'1) * q.((i+1)+1-'2) by F, C   .= p.(1+1-'1) * q.((i+1)+1-'2)
   .= p.1 * q.((i+1)+1-'2) by BINARITH:39 .= b * q.((i+1)+1-'2) by POLYNOM5:39
   .= b * q.(i+(1+1)-'2) by XCMPLX_1:1    .= b * q.(i+2-'2)
   .= b * q.i by BINARITH:39;
   now let k be Nat such that
   A1: 2 < k and
   B1: k in dom r;       k <> 0 by A1; then consider k1 being Nat such that
   C1: k = k1+1 by NAT_1:22;  2+1 <= k by A1, NAT_1:38; then
   D1: 2 <= k1 by C1, REAL_1:53;
    thus r.k = p.(k-'1) * q.((i+1)+1-'k) by B1, C
       .= p.k1 * q.((i+1)+1-'k) by C1, BINARITH:39
       .= (0.L) * q.((i+1)+1-'k) by D1, POLYNOM5:39 .= 0.L by VECTSP_1:39;
   end; then Sum r = r/.1 + r/.2 by D, thsum2;
 hence (<%a, b%>*'q).(i+1) = a*q.(i+1)+b*q.i by B, G, H;
end;

theorem LM3a: :: LM3a
for L being add-associative right_zeroed right_complementable distributive
            well-unital commutative associative 
            non degenerated (non empty doubleLoopStr),
    r being Element of L, q being non-zero Polynomial of L
 holds len (<%r, 1_ L%>*'q) = len q + 1
proof let L be add-associative right_zeroed right_complementable distributive
            well-unital commutative associative 
            non degenerated (non empty doubleLoopStr),
          r be Element of L, q being non-zero Polynomial of L;
   1_ L <> 0.L by VECTSP_1:def 21; then
B: len <%r, 1_ L%> = 2 by POLYNOM5:41;
   set p = <%r, 1_ L%>;
   len q > 0 by lenNZ; then
C: q.(len q -'1)<>0.L by LC1; 
   p.(len p -'1) * q.(len q -'1) = p.(1+1-'1) * q.(len q -'1) by B
   .= p.(1) * q.(len q -'1) by BINARITH:39
   .= 1_ L * q.(len q -'1) by POLYNOM5:39
   .= q.(len q -'1) by VECTSP_1:def 19;
 hence len (<%r, 1_ L%>*'q) = 2 + len q - 1 by B,C,POLYNOM4:13
    .= len q +(1+1)-1 .= len q +1+1-1 by XCMPLX_1:1 .= len q +1 by XCMPLX_1:26;
end;

theorem pexp2: :: pexp2
for L being non degenerated comRing, x being Element of L, i being Nat
 holds len (<%x, 1_ L%>`^i) = i+1
proof let L be non degenerated comRing, x be Element of L;
  defpred P[Nat] means  len (<%x, 1_ L%>`^$1) = $1+1;
  set r = <%x, 1_ L%>;
  r`^0 = 1_. L by POLYNOM5:16; then
BA: P[0] by POLYNOM4:7;
IS: for i being Nat st P[i] holds P[i+1] proof let i be Nat such that
    A1: P[i];
     i >= 0 by NAT_1:18; then i+1 > 0 by NAT_1:38; then
     reconsider ri = r`^i as non-zero Polynomial of L by A1, lenNZ;
     thus len (r`^(i+1)) = len ((r`^1)*'ri) by pexp1
       .= len (r*'ri) by POLYNOM5:17 .= i+1+1 by A1, LM3a;
    end;
  thus for i being Nat holds P[i] from Ind(BA,IS);
end;

definition
  let L be non degenerated comRing, x be Element of L, n be Nat;
  cluster <%x, 1_ L%>`^n -> non-zero;
  correctness proof len (<%x, 1_ L%>`^n) = n+1 by pexp2; then 
   len (<%x, 1_ L%>`^n) <> 0; then
   len (<%x, 1_ L%>`^n) > 0 by NAT_1:19;
   hence thesis by lenNZ;
  end;
end;

theorem pexp3: :: pexp3
for L being non degenerated comRing, x being Element of L,
    q being non-zero (Polynomial of L),  i being Nat
 holds len ((<%x, 1_ L%>`^i)*'q) = i + len q
proof let L being non degenerated comRing,  x being Element of L,
          q being non-zero Polynomial of L;
 set r = <%x, 1_ L%>;
 defpred P[Nat] means len ((r`^$1)*'q) = $1 + len q;
 len ((r`^0)*'q) = len ((1_. L)*'q) by POLYNOM5:16
 .= 0 + len q by POLYNOM3:36;  then
BA: P[0];
IS: for i being Nat st P[i] holds P[i+1] proof let i be Nat such that
    A1: P[i];
        0 <= i & len q > 0 by NAT_1:18, lenNZ; then i+len q > 0+0 by REAL_1:67;
        then
    B1: (r`^i)*'q is non-zero by A1, lenNZ;
     thus len ((r`^(i+1))*'q) = len ((r`^1)*'(r`^i)*'q) by pexp1
       .= len (r*'(r`^i)*'q) by POLYNOM5:17
       .= len (r*'((r`^i)*'q)) by POLYNOM3:34
       .= (i+len q)+1 by A1, B1, LM3a
       .= (i+1)+len q by XCMPLX_1:1;
    end;
 thus for i being Nat holds P[i] from Ind(BA,IS);
end;  

theorem LM3: :: LM3:
for L being add-associative right_zeroed right_complementable distributive
            well-unital commutative associative
            non degenerated (non empty doubleLoopStr),
    r being Element of L, p, q being Polynomial of L
 st p = <%r, 1_ L%>*'q & p.(len p -'1) = 1_ L holds q.(len q -'1) = 1_ L
proof let L be add-associative right_zeroed right_complementable distributive
            well-unital commutative associative
            non degenerated (non empty doubleLoopStr),
          x be Element of L, p, q be Polynomial of L such that
A: p = <%x, 1_ L%>*'q and
B: p.(len p -'1) = 1_ L;
   set lp1 = (len p -'1), lq1 = (len q -'1), d = <%x, 1_ L%>;
G: now assume q = 0_. L; then p = 0_. L by A, POLYNOM3:35; then
     p.(len p -'1) = 0.L by POLYNOM3:28;
    hence contradiction by B, VECTSP_1:def 21;
   end; then q is non-zero by LNZ; then
I: len p = len q + 1 by A, LM3a;
J: lp1 = len q by I, BINARITH:39; len q <> 0 by G, POLYNOM4:8; then
   consider lp2 being Nat such that
C: lp1 = lp2+1 by J, NAT_1:22;
D: lq1 = lp2 by C, J, BINARITH:39;
E: q.lp1 = 0.L by J, ALGSEQ_1:22;
   (<%x, 1_ L%>*'q).lp1 = x*q.(lp1)+(1_ L)*q.lp2 by C, f2mpoly
   .= 0.L +(1_ L)*q.lp2 by E, VECTSP_1:36
   .= (1_ L)*q.lp2 by RLVECT_1:10 .= q.lp2 by VECTSP_2:def 2;
 hence q.(len q -'1) = 1_ L by A, D, B;
end;

begin :: Little Bezout theorem

definition
  let L be non empty ZeroStr, p be Polynomial of L; let n be Nat;
  func poly_shift(p,n) -> Polynomial of L means                    :LPS:
    for i being Nat holds it.i = p.(n + i);
  existence proof
     deffunc F(Nat) = p.(n+$1);
     consider ps being AlgSequence of L such that
  A: len ps <= len p and
  B: for k being Nat st k < len p holds ps.k = F(k) from AlgSeqLambdaF;
     take ps; let i be Nat;
     per cases;
     suppose i < len p; hence ps.i = p.(n + i) by B; 
     suppose A1: i >= len p; then
     B1: i >= len ps by A, AXIOMS:22; 
     C1: n+i >= len p by A1, NAT_1:37;
      thus ps.i = 0.L by B1, ALGSEQ_1:22 .= p.(n + i) by C1, ALGSEQ_1:22; 
  end;
  uniqueness proof let it1, it2 be Polynomial of L such that
  A:     for i being Nat holds it1.i = p.(n + i) and
  B:     for i being Nat holds it2.i = p.(n + i);
   now let x be set; assume x in NAT; then
     reconsider i = x as Nat;
    thus it1.x = it1.i .= p.(n+i) by A .= it2.i by B .= it2.x;
   end;
   hence it1 = it2 by FUNCT_2:18;
  end;
end;

theorem PS0: :: PS0:
for L being non empty ZeroStr,p being Polynomial of L holds poly_shift(p,0) = p
proof let L be non empty ZeroStr, p be Polynomial of L;
   set ps = poly_shift(p,0);
   now let x be set; assume x in NAT; then reconsider i = x as Nat;
    thus ps.x = ps.i .= p.(0+i) by LPS .= p.x;
   end;
 hence poly_shift(p,0) = p by FUNCT_2:18;
end;

theorem PS1: :: PS1:
for L being non empty ZeroStr,  n being Nat, p being Polynomial of L
 st n >= len p holds poly_shift(p,n) = 0_. L
proof let L be non empty ZeroStr, n be Nat, p be Polynomial of L; assume
A: n >= len p;   set ps = poly_shift(p,n);
B: dom ps = NAT by FUNCT_2:def 1;
   now let z be set; assume z in dom ps; then reconsider i = z as Nat by B;
   B1: n+i >= len p by A, NAT_1:37;
    thus ps.z = ps.i .= p.(n+i) by LPS .= 0.L by B1, ALGSEQ_1:22;
   end; then ps = NAT --> 0.L by B, FUNCOP_1:17;
 hence poly_shift(p,n) = 0_. L by POLYNOM3:def 9;
end;

theorem PS2: :: PS2:
for L being non degenerated non empty multLoopStr_0,
    n being Nat, p being Polynomial of L
 st n <= len p holds len poly_shift(p,n) + n = len p
proof let L be non degenerated non empty multLoopStr_0,
          n be Nat, p be Polynomial of L such that
A: n <= len p;
   set ps = poly_shift(p,n), lpn = len p - n;
   n-n <= lpn by A, REAL_1:49; then 0 <= lpn by XCMPLX_1:14; then
   reconsider lpn as Nat by INT_1:16;
   now let i be Nat; assume i >= lpn; then
   A1: i+n >= len p by REAL_1:86;
    thus ps.i = p.(n+i) by LPS .= 0.L by A1, ALGSEQ_1:22;
   end; then
B: lpn is_at_least_length_of ps by ALGSEQ_1:def 3;
   now let m be Nat such that
   A1: m is_at_least_length_of ps and
   B1: lpn > m;       lpn >= m+1 by B1, NAT_1:38; then
       lpn -1 >= m +1-1 by REAL_1:49; then
   C1: lpn -1 >= m by XCMPLX_1:26;       0 <= m by NAT_1:18; then
       0 <= lpn -1 by C1; then  reconsider lpn1 = lpn -1 as Nat by INT_1:16;
   D1: (n+lpn1)+1 = n +(lpn1+1) by XCMPLX_1:1
       .= n+lpn by XCMPLX_1:27 .= len p by XCMPLX_1:27;
   F1: ps.lpn1 = p.(n+lpn1) by LPS; 
   E1: p.(n+lpn1) <> 0.L by D1, ALGSEQ_1:25;
       ps.lpn1 = 0.L by C1, A1, ALGSEQ_1:def 3;
    hence contradiction by E1, F1;
   end;
 hence len poly_shift(p,n) + n = lpn + n by B, ALGSEQ_1:def 4
    .= len p by XCMPLX_1:27;
end;

theorem evps: :: evps:
for L being  non degenerated comRing,
    x being Element of L, n being Nat, p being Polynomial of L
 st n < len p holds eval(poly_shift(p,n),x) = x*eval(poly_shift(p,n+1),x) + p.n
proof let L be non degenerated comRing,
          x being Element of L, n be Nat, p being Polynomial of L such that
AA: n < len p;
AAb: n <= len p by AA;
   set ps = poly_shift(p,n), ps1 = poly_shift(p,n+1);
   consider f be FinSequence of L such that
A: eval(ps,x) = Sum f and
B: len f = len ps and
C: for k be Nat st k in dom f holds f.k = ps.(k-'1) * (power L).(x,k-'1)
   by POLYNOM4:def 2;
   consider f1 be FinSequence of L such that
D: eval(ps1,x) = Sum f1 and
E: len f1 = len ps1 and
F: for k be Nat st k in dom f1 holds f1.k = ps1.(k-'1) * (power L).(x,k-'1)
   by POLYNOM4:def 2;
G: x*(Sum f1) = Sum (x*f1) by FVSUM_1:92;
H: x*f1 = (x multfield)*f1 by FVSUM_1:def 6;
   rng f1 c= the carrier of L & 
   dom (x multfield) = the carrier of L by FINSEQ_1:def 4, FUNCT_2:def 1; then
I: dom ((x multfield)*f1) = dom f1 by RELAT_1:46;
   now thus len f = len f;
   A1a: n+1 <= len p by AA, NAT_1:38; 
       len ps1 +1+n = len ps1 +(n+1) by XCMPLX_1:1
       .= len ps1 + (n+1) .= len p by A1a, PS2 .= len ps + n by AAb, PS2; then
   A1: len ps1 + 1 = len ps by XCMPLX_1:2;
   B1: len <*p.n*> = 1 by FINSEQ_1:57;
   C1: len ((x*f1)) = len f1 by I, H, FINSEQ_3:31;
   C1a: len (<*p.n*>^(x*f1)) = len (x*f1) + 1 by B1, FINSEQ_1:35;
    hence
   C1b: len (<*p.n*>^(x*f1)) = len f by A1, B, E, C1;
    let j be Nat such that
   D1: j in Seg len f;
   E1: j in dom f by D1, FINSEQ_1:def 3; then
   F1: 1 <= j & j <= len f by FINSEQ_3:27;
    per cases by F1, REAL_1:def 5;
    suppose S1: j = 1;
    G1: 1 in dom <*p.n*> by B1, FINSEQ_3:27;
     thus f.j = ps.(1-'1) * (power L).(x,1-'1) by E1, S1, C
       .= ps.0 * (power L).(x,1-'1) by GOBOARD9:1
       .= ps.0 * (power L).(x,0) by GOBOARD9:1 .= ps.0 * 1.L by GROUP_1:def 7
       .= ps.0 by GROUP_1:def 4 .= p.(n+0) by LPS .= <*p.n*>.1 by FINSEQ_1:57
       .= (<*p.n*>^(x*f1)).j by S1, G1, FINSEQ_1:def 7;
    suppose 1 < j; then
    G1: 1+1 <= j by NAT_1:38; 1-1 <= j-1 by F1, REAL_1:49; then 0 <= j-1; then
        reconsider j1 = j-1 as Nat by  INT_1:16;
    I1a: 1+1-1 <= j-1 by G1, REAL_1:49;
        j-1 <= len f1 + 1-1 by F1, C1a, C1, C1b, REAL_1:49; then
    J1: 1 <= j1 & j1 <= len f1 by I1a, XCMPLX_1:26; then
    J1a: j1 in dom f1 by FINSEQ_3:27; then
        reconsider f1j = f1.j1 as Element of L by FINSEQ_2:13;
        j = j1+1 by XCMPLX_1:27; then
    K1a: j1 = j-'1 by BINARITH:39;
        0 < j1 by J1, AXIOMS:22; then
        consider j2 being Nat such that
    Ma: j1 = j2+1 by NAT_1:22;
    M: j1-'1+1 = j2+1 by Ma, BINARITH:39 .= j1 by Ma;
    L: (n+1)+(j1-'1) = n+(1+(j1-'1)) by XCMPLX_1:1 .= n+j1 by M;
     thus f.j = ps.(j-'1) * (power L).(x,j-'1) by E1, C
      .= p.(n+j1) * (power L).(x,j1) by K1a, LPS
      .= p.((n+1)+(j1-'1)) * (((power L).(x,j1-'1)) * x) by L,M,GROUP_1:def 7
      .= (p.((n+1)+(j1-'1))*(power L).(x,j1-'1)) * x by VECTSP_1:def 16
      .= x*(p.((n+1)+(j1-'1)) * (power L).(x,j1-'1))
      .= x*(ps1.(j1-'1) * (power L).(x,j1-'1)) by LPS .= x*f1j by J1a, F
      .= (x*f1).j1 by J1a, I, H, FVSUM_1:62
      .= (<*p.n*>^(x*f1)).j by G1, B1, C1a, F1, C1b, FINSEQ_1:36;
   end; then f = <*p.n*>^(x*f1)by FINSEQ_2:10;
 hence eval(poly_shift(p,n),x) =  p.n + x*eval(poly_shift(p,n+1),x)
      by A, D, G, FVSUM_1:89
      .= x*eval(poly_shift(p,n+1),x) + p.n;
end;

theorem Roots0: :: Roots0:
for L being non degenerated comRing, p being Polynomial of L
 st len p = 1 holds Roots p = {}
proof let L be non degenerated comRing,  p be Polynomial of L; assume
A: len p = 1; assume Roots p <> {}; then consider x being set such that
B: x in Roots p by XBOOLE_0:def 1;
C: p =<%p.0%> & p.0 <> 0.L by A, plen1;  reconsider x as Element of L by B;
   x is_a_root_of p by B,POLYNOM5:def 9;then eval(p,x) = 0.L by POLYNOM5:def 6;
 hence contradiction by C, POLYNOM5:38;
end; 

definition
  let L be non degenerated comRing, r be Element of L,  p be Polynomial of L
  such that A: r is_a_root_of p;
  func poly_quotient(p,r) -> Polynomial of L means                      :LPQUO:
     len it + 1 = len p &
     for i being Nat holds it.i = eval(poly_shift(p, i+1),r) if len p > 0
  otherwise it = 0_. L;
  existence proof
   hereby assume B: len p > 0; consider p1 being Nat such that
  F: len p = p1+1 by B, NAT_1:22;     set lq = len p -'1;
  Fa: lq = p1 by F, BINARITH:39;
  Aa: len p >= 0+1 by B, NAT_1:38;   r in Roots p by A, POLYNOM5:def 9; then
      Roots p <> {}; then  len p <> 1 by Roots0; then
      len p > 0+1 by Aa, REAL_1:def 5; then lq > 0 by F, Fa, AXIOMS:24;
      then consider lq1 being Nat such that
  Ab: lq = lq1 + 1 by NAT_1:22;
  Ac: lq1 = lq -'1 by Ab, BINARITH:39;
  Ad: lq < len p by Fa, F, NAT_1:38;
     deffunc F(Nat) = eval(poly_shift(p, $1+1),r);
     consider q being Function of NAT, the carrier of L such that
  Ba: for k being Nat holds q.k = F(k) from LambdaD;
     reconsider q as sequence of L by NORMSP_1:def 3;
       q.lq1 = eval(poly_shift(p, lq1+1),r) by Ba
            .= r*eval(poly_shift(p, len p),r) + p.lq by Ab,Ad,Fa,F,evps
            .= r*eval(0_. L,r) + p.lq by PS1 .= r*0.L + p.lq by POLYNOM4:20
            .= 0.L + p.lq by VECTSP_1:36 .= p.lq by RLVECT_1:10; then
  Bd: q.lq1 <> 0.L by F, Fa, ALGSEQ_1:25;
  Bc: now let i be Nat such that
      A1: i >= lq;          i >= p1+1 -' 1 by A1, F; then
          i >= p1 by BINARITH:39; then
      B1: i+1 >= len p by F, AXIOMS:24;
          thus q.i = eval(poly_shift(p, i+1),r) by Ba
           .= eval(0_.L,r) by B1, PS1 .= 0.L by POLYNOM4:20;
      end; then reconsider q as AlgSequence of L by ALGSEQ_1:def 2;
     take q;
  C: lq is_at_least_length_of q by Bc, ALGSEQ_1:def 3;
     now let m be Nat; assume m is_at_least_length_of q; then
     B1: for i being Nat st i >= m holds q.i = 0.L by ALGSEQ_1:def 3;
       assume
     C1: lq > m; 0 <= m by NAT_1:18; then
       lq > 0 by C1; then consider lq1 being Nat such that
     D1: lq = lq1 + 1 by NAT_1:22;  lq >= m+1 by C1, NAT_1:38; then
     E1: lq1 >= m by D1, REAL_1:53; lq1 = lq-'1 by D1, BINARITH:39; then
       lq -'1 >= m by E1; then q.(lq-'1) = 0.L by B1;
      hence contradiction by Ac, Bd;
     end; then
  E: len q = lq by C, ALGSEQ_1:def 4; 
   thus len q + 1 = len p -'1+1 by E .=p1+1-'1+1 by F .=len p by F,BINARITH:39;
   thus for k being Nat holds q.k = F(k) by Ba;
   end;
   thus thesis;
  end;
  uniqueness proof let it1, it2 be Polynomial of L;
   hereby assume len p > 0; assume that
  A: len it1 + 1 = len p &
     for i being Nat holds it1.i = eval(poly_shift(p, i+1),r) and
  B: len it2 + 1 = len p &
     for i being Nat holds it2.i = eval(poly_shift(p, i+1),r);
  C: len it1 = len it1 +1-1 by XCMPLX_1:26 .= len it2 by A, B, XCMPLX_1:26;
     now let k be Nat such that k < len it1;
      thus it1.k = eval(poly_shift(p, k+1),r) by A .= it2.k by B;
     end;
    hence it1 = it2 by C, ALGSEQ_1:28;
   end;
   thus thesis;
  end;
  consistency;
end;

theorem pqlen: :: pqlen:
for L being non degenerated comRing,
    r being Element of L, p being non-zero Polynomial of L
 st r is_a_root_of p holds len poly_quotient(p,r) > 0 
proof let L be non degenerated comRing,
          r be Element of L, p be non-zero Polynomial of L such that
B: r is_a_root_of p;
A: len p > 0 by lenNZ;
Ca: len poly_quotient(p,r) + 1 = len p by A, B, LPQUO;
C: len poly_quotient(p,r) >= 0 by NAT_1:18;
  assume len poly_quotient(p,r) <= 0; then
  len poly_quotient(p,r) = 0 by C; then
D: Roots p = {} by Ca, Roots0; 
   r in Roots p by B, POLYNOM5:def 9;
 hence contradiction by D;
end;

theorem Roots1: :: Roots1:
for L being add-associative right_zeroed right_complementable
            left-distributive well-unital (non empty doubleLoopStr),
    x being Element of L
 holds Roots <%-x, 1_ L%> = {x}
proof let L be add-associative right_zeroed right_complementable
            left-distributive well-unital (non empty doubleLoopStr),
          x be Element of L;
 now let a be set;
   hereby assume
   A: a in Roots <%-x, 1_ L%>; then
      reconsider b = a as Element of L;
      b is_a_root_of <%-x, 1_ L%> by A, POLYNOM5:def 9; then
      0.L = eval(<%-x, 1_ L%>,b) by POLYNOM5:def 6
         .= -x + b by POLYNOM5:48; then -x = -b by RLVECT_1:19;
    hence x = a by RLVECT_1:31;
   end;
   assume A: a = x;
    eval(<%-x, 1_ L%>,x) = -x + x by POLYNOM5:48 .= 0.L by RLVECT_1:16; then
    x is_a_root_of <%-x, 1_ L%> by POLYNOM5:def 6;
  hence a in Roots <%-x, 1_ L%> by A, POLYNOM5:def 9;
 end;
 hence Roots <%-x, 1_ L%> = {x} by TARSKI:def 1;
end; 

theorem BZA: :: BZA:
for L being non trivial comRing,
    x being Element of L, p, q  being Polynomial of L
 st p = <%-x,1_ L%>*'q holds x is_a_root_of p
proof let L be non trivial comRing,
          x be Element of L, p, q  be Polynomial of L such that
A: p = <%-x,1_ L%>*'q;
B: eval(<%-x,1_ L%>,x) = (-x)+x by POLYNOM5:48 .= 0.L by RLVECT_1:16;
 thus eval(p,x) = eval(<%-x,1_ L%>,x) * eval(q,x) by A, POLYNOM4:27
               .= 0.L by B, VECTSP_1:39;
end;

theorem  BEZOUT: :: Factor theorem (Bezout) 
for L being non degenerated comRing,
    r being Element of L, p being Polynomial of L
 st r is_a_root_of p holds p = <%-r,1_ L%>*'poly_quotient(p,r)
proof let L be non degenerated comRing,
          x be Element of L, p be Polynomial of L; assume that
B: x is_a_root_of p;
   set r = <%-x,1_ L%>, pq = poly_quotient(p,x);
Aa: len p >= 0 by NAT_1:18;
   per cases by Aa;
   suppose A: len p > 0;
      0.L <> 1_ L by VECTSP_1:def 21; then
C: len r = 2 by POLYNOM5:41;
   p is non-zero by A, lenNZ; then
   len pq > 0 by B, pqlen; then
Da: pq.(len pq -'1) <> 0.L by LC1;
    r.(len r -'1) = r.(1+1-'1) by C .= r.1 by BINARITH:39
    .= 1_ L by POLYNOM5:39; then
Db: r.(len r -'1) * pq.(len pq -'1) = pq.(len pq -'1) by VECTSP_1:def 19; 
  now len (r *' pq) = len r + len pq - 1 by Db, Da, POLYNOM4:13
   .= len pq +(1+1)-1 by C .= len pq +1+1- 1 by XCMPLX_1:1
   .= len pq +1 by XCMPLX_1:26 .= len p by A, B, LPQUO; 
   hence len p = len (r *' pq);
   let k be Nat; assume k < len p;
   defpred P[Nat] means p.$1 = (r*'pq).$1;
E: (r*'pq).0 = (-x)*pq.0 by f2mpoly
            .= (-x)*eval(poly_shift(p, 0+1),x) by A, B, LPQUO;
F: 0.L = eval(p,x) by B, POLYNOM5:def 6 .= eval(poly_shift(p,0),x) by PS0
      .= x*eval(poly_shift(p,0+1),x) + p.0 by A, evps;
   (-x)*eval(poly_shift(p, 0+1),x)
     = (-x)*eval(poly_shift(p, 0+1),x) + 0.L by RLVECT_1:def 7
    .= (-x)*eval(poly_shift(p, 0+1),x) + x*eval(poly_shift(p,1),x) + p.0
       by F, RLVECT_1:def 6
    .= -x*eval(poly_shift(p, 0+1),x) + x*eval(poly_shift(p,1),x) + p.0
       by VECTSP_1:41    .= 0.L +p.0 by RLVECT_1:16 .= p.0 by RLVECT_1:10; then
  BA: P[0] by E;
  IS: for k being Nat st P[k] holds P[k+1] proof
       let k be Nat; assume P[k];
      C1: pq.(k+1) = eval(poly_shift(p, k+1+1),x) by A, B, LPQUO;
      B1: pq.k = eval(poly_shift(p, k+1),x) by A, B, LPQUO;
      per cases;
      suppose A1a: k+1 >= len p; then
      D1: pq.k = eval(0_.L,x) by B1, PS1 .= 0.L by POLYNOM4:20;
          k+1 <= k+1+1 by NAT_1:37; then k+1+1 >= len p by A1a, AXIOMS:22; then
      E1: pq.(k+1) = eval(0_.L,x) by C1, PS1 .= 0.L by POLYNOM4:20;
        (r*'pq).(k+1) = (-x)*pq.(k+1)+(1_ L)*pq.k by f2mpoly
      .= 0.L + (1_ L)*pq.k by E1, VECTSP_1:36
      .= 0.L + 0.L by D1, VECTSP_1:36 .= 0.L by RLVECT_1:10;
       hence P[k+1] by A1a, ALGSEQ_1:22;               
      suppose A1a: k+1 < len p;
          pq.k = x*eval(poly_shift(p, k+1+1),x) + p.(k+1) by B1,A1a, evps; then
      D1: -x*pq.(k+1)+pq.k
        = -x*pq.(k+1)+x*eval(poly_shift(p, k+1+1),x)+p.(k+1) by RLVECT_1:def 6
       .= 0.L + p.(k+1) by C1, RLVECT_1:16;
         (r*'pq).(k+1) = (-x)*pq.(k+1)+(1_ L)*pq.k by f2mpoly
      .= (-x)*pq.(k+1)+pq.k by VECTSP_1:def 19
      .= -x*pq.(k+1)+pq.k by VECTSP_1:41;
       hence P[k+1] by D1, RLVECT_1:10;
      end;    for k being Nat holds P[k] from Ind(BA,IS);
   hence p.k = (r*'pq).k;
  end;
 hence p = r*'pq by ALGSEQ_1:28;
 suppose len p = 0; then pq = 0_. L & p = 0_. L by POLYNOM4:8, B, LPQUO;
  hence thesis by POLYNOM3:35;
end;

theorem  BEZOUTa: :: Factor theorem (Bezout) 
for L being non degenerated comRing,
    r being Element of L, p, q being Polynomial of L
 st p = <%-r,1_ L%>*'q holds r is_a_root_of p 
proof let L be non degenerated comRing,
          r be Element of L, p, q be Polynomial of L;
 assume p = <%-r,1_ L%>*'q;
 then eval(p,r) = eval(<%-r,1_ L%>,r) * eval(q,r) by POLYNOM4:27
            .= (-r+r) * eval(q,r) by POLYNOM5:48
            .= 0.L * eval(q,r) by RLVECT_1:def 10
            .= 0.L by VECTSP_1:39;
 hence thesis by POLYNOM5:def 6;
end;

BZBL: now let L be domRing, p be non-zero Polynomial of L;
   p <> 0_. L by LNZ; then len p <> 0 by POLYNOM4:8; then
   len p > 0 by NAT_1:19; then
A: len p >= 0+1 by NAT_1:38;
  defpred P[Nat] means
  for p being Polynomial of L st len p = $1 holds
  Roots p is finite &
  ex n being Nat st n = Card Roots p & n < len p;
BA: P[1] proof let p be Polynomial of L; assume
    B1: len p = 1; then
    A1: Roots p = {} by Roots0;
     thus Roots p is finite by A1;
     take 0; thus 0 = Card Roots p by A1, CARD_1:78; thus 0 < len p by B1;
    end; 
IS: for n being Nat st n>=1 & P[n] holds P[n+1] proof
     let n be Nat such that
    A1: n >= 1 and
    B1: P[n];     let p be Polynomial of L; assume
    C1a: len p = n+1; then
    C1: len p > 1 by A1, NAT_1:38;
    per cases;
    suppose p is with_roots; then
        consider x being Element of L such that
    D1: x is_a_root_of p by POLYNOM5:def 7;
    D1a: len p > 0 by C1, AXIOMS:22;
    E1: p = <%-x,1_ L%>*'poly_quotient(p,x) by D1, BEZOUT;
        set r = <%-x,1_ L%>, pq = poly_quotient(p,x);
        len pq + 1 = len p by D1, D1a, LPQUO; then
    H1: len pq = n by C1a, XCMPLX_1:2; then
    F1: Roots pq is finite by B1;
    G1: Roots r = {x} by Roots1;
    K1: Roots p = (Roots r)\/Roots pq by E1,pdomring0;
     hence Roots p is finite by F1, G1, FINSET_1:14;
        consider k being Nat such that
    I1: k = Card Roots pq and
    J1: k < len pq by B1, H1;
        reconsider Rpq = Roots pq as finite set by B1, H1;
        reconsider Rr = Roots r as finite set by G1;
        reconsider Rp = Rpq \/ Rr as finite set;
        take m = card Rp; thus m = Card Roots p by K1;
         card Rr = 1 by G1, CARD_1:79; then
    L1:  card Rp <= k + 1 by I1, CARD_2:62;
         k+1 < n+1 by J1, H1, REAL_1:67;
       hence m < len p by C1a, L1, AXIOMS:22;
    suppose S1: not p is with_roots; 
    A1: now assume Roots p <> {}; then consider x being set such that
        A2: x in Roots p by XBOOLE_0:def 1;
            reconsider x as Element of L by A2;
            x is_a_root_of p by A2, POLYNOM5:def 9;
         hence contradiction by S1, POLYNOM5:def 7;
        end;
     thus Roots p is finite by A1;
     take 0; thus 0 = Card Roots p by A1, CARD_1:78;
     thus 0 < len p by C1, AXIOMS:22;     
    end;
  for n being Nat st n >= 1 holds P[n] from Ind1(BA,IS);
  hence Roots p is finite & 
        ex n being Nat st n = Card Roots p & n < len p by A;
end;

begin :: Polynomials defined by roots

definition  :: It is not true for a comRing. Who knows an example?
  let L be domRing, p be non-zero Polynomial of L;
  cluster Roots p -> finite;
  correctness by BZBL;
end; 

definition
  let L be non degenerated comRing, x be Element of L,
      p be non-zero (Polynomial of L);
  func multiplicity(p,x) -> Nat means                              :MultiDef:
  ex F being finite non empty Subset of NAT
   st F = {k where k is Nat : ex q being Polynomial of L
                      st p = (<%-x, 1_ L%>`^k) *' q} &
      it = max F;
  existence proof
A: len p > 0 by lenNZ;
   set r = <%-x, 1_ L%>;
   defpred P[Nat] means ex q being Polynomial of L st p = (r`^$1) *' q;
   set F = {k where k is Nat : P[k]};
   p = (1_. L) *' p by POLYNOM3:36 .= (r`^0) *' p by POLYNOM5:16; then
  A1: 0 in F;
  B1: F c= len p proof let a be set; assume a in F; then
         consider k being Nat such that
      A2: a = k and
      B2: P[k];          consider q being Polynomial of L such that
      C2: p = (r`^k) *' q by B2;
          now assume len q = 0; then q = 0_. L by POLYNOM4:8; then
            p = 0_. L by C2, POLYNOM4:5; then len p = 0 by POLYNOM4:6;
           hence contradiction by A;
          end; then
      D2: len q > 0 by NAT_1:19;
          then reconsider q as non-zero Polynomial of L by lenNZ;
          now assume k >= len p; then
            k+len q > len p + 0 by D2, REAL_1:67;
           hence contradiction by C2, pexp3;
          end; then k in {i where i is Nat : i < len p};
        hence a in len p by A2, AXIOMS:30;
      end;   F c= NAT from Fr_Set0; then
   reconsider F as finite non empty Subset of NAT by A1, B1, FINSET_1:13;
   reconsider FF = F as finite non empty natural-membered set;
   max FF in NAT by ORDINAL2:def 21; then
   reconsider m = max FF as Nat;
   take m; thus thesis;
  end;
  uniqueness;
end;

theorem MULTI1: :: MULTI1:
for L being non degenerated comRing,
    p being non-zero (Polynomial of L), x being Element of L
 holds x is_a_root_of p iff multiplicity(p,x) >= 1
proof let L be non degenerated comRing, 
    p being non-zero (Polynomial of L), x being Element of L;
    set r = <%-x, 1_ L%>; set m = multiplicity(p,x);
   consider F being finite non empty Subset of NAT such that
B: F = {k where k is Nat : ex q being Polynomial of L st p = (r`^k) *' q} and
C: m = max F by MultiDef;
 hereby assume x is_a_root_of p; then
 A1: p = r*'poly_quotient(p,x) by BEZOUT;
     r`^1 = r by POLYNOM5:17; then 1 in F by B, A1; 
  hence multiplicity(p,x) >= 1 by C, PRE_CIRC:def 1;
 end;
 assume
 A1: multiplicity(p,x) >= 1;
     m in F by C, PRE_CIRC:def 1; then consider k being Nat such that
 B1: m = k and
 C1: ex q being Polynomial of L st p = (r`^k) *' q by B;
     consider q being Polynomial of L such that
 D1: p = (r`^k) *' q by C1; m <> 0 by A1; then
     consider k1 being Nat such that
 E1: k = k1+1 by B1, NAT_1:22;
     p = r *' (r`^k1) *' q by D1, E1, POLYNOM5:20
      .= r *' ((r`^k1) *' q) by POLYNOM3:34;
 hence x is_a_root_of p by BZA;
end;

theorem MULTI2: :: MULTI2:
for L being non degenerated comRing,
    x being Element of L holds multiplicity(<%-x, 1_ L%>,x) = 1
proof let L be non degenerated comRing, x be Element of L;
   set r = <%-x, 1_ L%>;   0.L <> 1_ L by VECTSP_1:def 21; then
A: len r = 2 by POLYNOM5:41;
   consider F being finite non empty Subset of NAT such that
B: F = {k where k is Nat : ex q being Polynomial of L st r = (r`^k) *' q} and
C: multiplicity(r,x) = max F by MultiDef;
   r = (r`^1) by POLYNOM5:17; then r = (r`^1) *' 1_. L by POLYNOM3:36; then
   1 in F by B; then
D: multiplicity(r,x) >= 1 by C, PRE_CIRC:def 1;
   set j = multiplicity(r,x);   j in F by C, PRE_CIRC:def 1; then
   consider k being Nat such that
E: k = j and
F: ex q being Polynomial of L st r = (r`^k) *' q by B;
   consider q being Polynomial of L such that
G: r = (r`^k) *' q by F;
   now assume len q = 0; then q = 0_. L by POLYNOM4:8; then
     r = 0_. L by G, POLYNOM4:5; then len r = 0 by POLYNOM4:6;
    hence contradiction by A;
   end; then
H: len q > 0 by NAT_1:19; then
Ha: q is non-zero by lenNZ;
J: 2 = k+len q by Ha, G, A, pexp3;
   now assume k > 1; then k >= 1+1 by NAT_1:38; then
       k+len q > 2+0 by H, REAL_1:67;
    hence contradiction by J;
   end;
 hence multiplicity(<%-x, 1_ L%>,x) = 1 by D, E, REAL_1:def 5;
end;

definition
  let L be domRing, p be non-zero Polynomial of L;
  func BRoots(p) -> bag of the carrier of L means                    :LBRoots:
   support it = Roots p &
   for x being Element of L holds it.x = multiplicity(p,x);
  existence proof
    deffunc F(Element of L) = multiplicity(p,$1);
    consider b being Function of the carrier of L, NAT such that
  A: for x being Element of L holds b.x = F(x) from LambdaD;
  Ba: dom b = the carrier of L by FUNCT_2:def 1; then
  B: b is ManySortedSet of the carrier of L by PBOOLE:def 3;
  C: support b c= the carrier of L by Ba, POLYNOM1:41;
   now let x be set;
    hereby assume
   A1: x in support b; then
   B1: b.x <> 0 by POLYNOM1:def 7; reconsider xx = x as Element of L by A1, C;
   C1: b.x = F(xx) by A; 0 < b.xx by B1, NAT_1:19;
       then b.xx >= 0+1 by NAT_1:38; then xx is_a_root_of p by C1, MULTI1;
    hence x in Roots p by POLYNOM5:def 9;
   end;
   assume A1: x in Roots p; then
     reconsider xx = x as Element of L; xx is_a_root_of p by A1,POLYNOM5:def 9;
     then multiplicity(p,xx) >= 1 by MULTI1; then b.xx >= 1 by A; then
     b.xx <> 0;
    hence x in support b by POLYNOM1:def 7;
    end; then
  Z: support b = Roots p by TARSKI:2; then support b is finite; then
  C: b is finite-support by POLYNOM1:def 8;
     reconsider b as bag of the carrier of L by B, C;
     take b;     thus thesis by Z, A;
  end;
  uniqueness proof let it1, it2 be bag of the carrier of L such that
         support it1 = Roots p and
  A1:    for x being Element of L holds it1.x = multiplicity(p,x) and
         support it2 = Roots p and
  B1:    for x being Element of L holds it2.x = multiplicity(p,x);
    now let x be set; assume x in the carrier of L; then
        reconsider xx = x as Element of L;
     thus it1.x = multiplicity(p,xx) by A1 .= it2.x by B1;
    end;
   hence it1 = it2 by PBOOLE:3;
  end;
end;

theorem BR1e: :: BR1e:
for L being domRing, x being Element of L
 holds BRoots <%-x, 1_ L%> = ({x}, 1)-bag
proof let L be domRing, x be Element of L;
  set r = <%-x, 1_ L%>;   0.L <> 1_ L by VECTSP_1:def 21; then
   Roots r = {x} by Roots1; then
B: support BRoots r = {x} by LBRoots;
C: x in {x} by TARSKI:def 1;
   now let i be set; assume i in the carrier of L; then
       reconsider i1 = i as Element of L;
    per cases;
    suppose B1: i = x;
    thus (BRoots r).i = multiplicity(r,i1) by LBRoots
        .= 1 by B1, MULTI2       .= (({x}, 1)-bag).i by B1, C, Snbag1;
    suppose i <> x; then
    C1: not i in {x} by TARSKI:def 1;
      hence (BRoots r).i = 0 by B, POLYNOM1:def 7
         .= (({x}, 1)-bag).i by C1, Snbag0;
   end;
 hence BRoots <%-x, 1_ L%> = ({x}, 1)-bag by PBOOLE:3;
end;

theorem BR1da: :: BR1da:
for L being domRing, x be Element of L, p, q being non-zero Polynomial of L
  holds multiplicity(p*'q,x) = multiplicity(p,x) + multiplicity(q,x)
proof let L be domRing,x be Element of L,  p, q being non-zero Polynomial of L;
   set r = <%-x, 1_ L%>;
   consider F being finite non empty Subset of NAT such that
D:  F = {k where k is Nat : ex pqq being Polynomial of L
                             st p*'q = (r`^k) *' pqq} and
E: multiplicity(p*'q,x) = max F by MultiDef;
   consider f being finite non empty Subset of NAT such that
F:  f = {k where k is Nat : ex pq being Polynomial of L
                      st p = (r`^k) *' pq} and
G: multiplicity(p,x) = max f by MultiDef;
   consider g being finite non empty Subset of NAT such that
H:  g = {k where k is Nat : ex qq being Polynomial of L
                      st q = (r`^k) *' qq} and
I: multiplicity(q,x) = max g by MultiDef;
   max F in F by PRE_CIRC:def 1; then
   consider k being Nat such that
Da: k = max F and
Db: ex pqq being Polynomial of L st p*'q = (r`^k) *' pqq by D;
    consider pqq being Polynomial of L such that
Dc: p*'q = (r`^k) *' pqq by Db;
   max f in f by PRE_CIRC:def 1; then
   consider i being Nat such that
Fa: i = max f and
Fb: ex pq being Polynomial of L st p = (r`^i) *' pq by F;
    consider pq being Polynomial of L such that
Fc: p = (r`^i) *' pq by Fb;
   max g in g by PRE_CIRC:def 1; then
   consider j being Nat such that
Ga: j = max g and
Gb: ex qq being Polynomial of L st q = (r`^j) *' qq by H;
    consider qq being Polynomial of L such that
Gc: q = (r`^j) *' qq by Gb;
K:  p*'q = (r`^i) *' pq *' ((r`^j) *' qq) by Fc, Gc
        .= (r`^i) *' pq *' (r`^j) *' qq by POLYNOM3:34
        .= (r`^i) *' (pq *' (r`^j)) *' qq by POLYNOM3:34
        .= (r`^i) *' (r`^j) *' pq  *' qq by POLYNOM3:34
        .= (r`^(i+j)) *' pq  *' qq by pexp1
        .= (r`^(i+j)) *' (pq  *' qq) by POLYNOM3:34;
   then i+j in F by D; then
J: i+j <= k by Da, PRE_CIRC:def 1;
   now assume i+j < k; then 0+(i+j) < k; then
   B1: 0 < k-(i+j) by REAL_1:86; then       0 <= k-(i+j); then
       reconsider kij = k-(i+j) as Nat by INT_1:16;
       consider kk being Nat such that
   D1: kij = kk+1 by B1, NAT_1:22;
       (0_. L).1 = 0.L & r.1 = 1_ L by POLYNOM3:28, POLYNOM5:39; then
       r <> 0_. L by VECTSP_1:def 21; then
   C1: r`^(i+j) <> 0_. L by pexp0;
       k = kij + (i+j) by XCMPLX_1:27; then
       p*'q = ((r`^(i+j)) *' (r`^kij)) *' pqq by Dc, pexp1
           .= (r`^(i+j)) *' ((r`^kij) *' pqq) by POLYNOM3:34; then
   E1: (r`^kij) *' pqq = pq  *' qq by C1, K, pcanc0;
       (r`^kij) = (r`^1) *' (r`^kk) by D1, pexp1
               .= r *' (r`^kk) by POLYNOM5:17; then
       (r`^kij) *' pqq = r *' ((r`^kk) *' pqq) by POLYNOM3:34; then
       x is_a_root_of (pq  *' qq) by E1, BZA; then
       x in Roots (pq  *' qq) by POLYNOM5:def 9; then
       x in (Roots pq \/ Roots qq) by pdomring0; then
   F1: x in Roots(pq) or x in Roots(qq) by XBOOLE_0:def 2;
    per cases by F1;
    suppose x in Roots(pq); then x is_a_root_of pq by POLYNOM5:def 9; then
      pq = r *' poly_quotient(pq,x) by BEZOUT; then
      p = (r`^i) *' r *' poly_quotient(pq,x) by Fc, POLYNOM3:34
       .= (r`^i) *' (r`^1) *' poly_quotient(pq,x) by POLYNOM5:17
       .= (r`^(i+1)) *' poly_quotient(pq,x) by pexp1; then
      i+1 in f by F; then      i+1 <= i by Fa, PRE_CIRC:def 1;
     hence contradiction by NAT_1:38;
    suppose x in Roots(qq); then x is_a_root_of qq by POLYNOM5:def 9; then
      qq = r *' poly_quotient(qq,x) by BEZOUT; then
      q = (r`^j) *' r *' poly_quotient(qq,x) by Gc, POLYNOM3:34
       .= (r`^j) *' (r`^1) *' poly_quotient(qq,x) by POLYNOM5:17
       .= (r`^(j+1)) *' poly_quotient(qq,x) by pexp1; then
      j+1 in g by H; then j+1 <= j by Ga, PRE_CIRC:def 1;
     hence contradiction by NAT_1:38;
   end;
  hence multiplicity(p*'q,x) = multiplicity(p,x) + multiplicity(q,x)
     by J, Da, Fa, Ga, E, G, I, REAL_1:def 5;
end;

theorem BR1d: :: BR1d:
for L being domRing, p, q being non-zero Polynomial of L
 holds BRoots(p*'q) = BRoots(p) + BRoots(q)
proof let L be domRing, p, q being non-zero Polynomial of L;
   now let i be set; assume
   A1: i in the carrier of L;
      reconsider x = i as Element of L by A1;
    thus (BRoots(p*'q)).i = multiplicity(p*'q, x) by LBRoots
       .= multiplicity(p,x) + multiplicity(q,x) by BR1da
       .= (BRoots p).i + multiplicity(q,x) by LBRoots
       .= (BRoots p).i + (BRoots q).i by LBRoots
       .= (BRoots(p) + BRoots(q)).i by POLYNOM1:def 5;       
   end; 
 hence BRoots(p*'q) = BRoots(p) + BRoots(q) by PBOOLE:3;
end;

BR1a:
now let L be domRing, p, q be non-zero Polynomial of L; 
   BRoots(p*'q) = BRoots(p) + BRoots(q) by BR1d;
 hence degree BRoots (p*'q) = degree (BRoots p) + degree BRoots q by BAGDEG2;
end;

theorem BR1b: :: BR1b:
for L being domRing, p being non-zero Polynomial of L
 st len p = 1 holds degree BRoots p = 0
proof let L be domRing, p being non-zero Polynomial of L; assume
   len p = 1; then Roots p = {} by Roots0; then
   support BRoots p = {} by LBRoots; then
   BRoots p = EmptyBag the carrier of L by BAGORDER:20;
 hence degree BRoots p = 0 by BAGDEG0;
end;

theorem BR1c: :: BR1c:
for L being domRing, x be Element of L, n being Nat
 holds degree BRoots (<%-x, 1_ L%>`^n) = n
proof let L be domRing, x be Element of L;
  set r = <%-x, 1_ L%>;
  defpred P[Nat] means degree BRoots (r`^$1) = $1;
  A: len 1_. L = 1 by POLYNOM4:7;
  B: r`^0 = 1_. L by POLYNOM5:16;
BA: P[0] by BR1b, A, B;
IS: for n being Nat st P[n] holds P[n+1] proof let n be Nat such that
    A: P[n];       0.L <> 1_ L by VECTSP_1:def 21; then
       card {x} = 1 & support ({x},1)-bag = {x} by Snbagsup, CARD_1:79; then
    D: degree ({x},1)-bag = 1 by BAGDEG1;
       r`^(n+1) = (r`^n)*'r by POLYNOM5:20; then
       degree BRoots(r`^(n+1))
       = degree BRoots (r`^n) + degree BRoots r by BR1a
      .= n + degree ({x},1)-bag by A, BR1e;
     hence P[n+1] by D;
    end;
 thus for n being Nat holds P[n] from Ind(BA,IS);
end;

theorem :: BR2
for L being algebraic-closed domRing, p being non-zero Polynomial of L
 holds degree BRoots p = len p -' 1
proof  let L be algebraic-closed domRing, p be non-zero Polynomial of L;
A: len p > 0 by lenNZ;
    defpred P[Nat] means
    for p being non-zero Polynomial of L st len p = $1 & $1 > 0
     holds degree BRoots p = len p -' 1;
P: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
   proof let k be Nat; assume
   A1: for n being Nat st n < k holds P[n];
    let p be non-zero Polynomial of L; assume that
   B1: len p = k and
   C1b: k > 0;
   C1a: k >= 0+1 by C1b, NAT_1:38;
    thus thesis proof per cases by C1a, REAL_1:def 5;
    suppose S1: k = 1;
     hence degree BRoots p = 0 by B1, BR1b .= 1-1
        .= len p -' 1 by B1, S1, SCMFSA_7:3;
     suppose C1: k > 1;
       p is with_roots by B1, C1, POLYNOM5:def 8;  then
       consider x being Element of L such that
   D1: x is_a_root_of p by POLYNOM5:def 7;
   E1: multiplicity(p,x) >= 1 by D1, MULTI1;
       consider F being finite non empty Subset of NAT such that
   F1: F = {l where l is Nat : ex q being Polynomial of L
                      st p = (<%-x, 1_ L%>`^l) *' q} and
   G1: multiplicity(p,x) = max F by MultiDef;
       max F in F by PRE_CIRC:def 1; then
       consider l being Nat such that
   J1: l = max F and
   K1: ex q being Polynomial of L st p = (<%-x, 1_ L%>`^l) *' q by F1;
       consider q being Polynomial of L such that
   L1: p = (<%-x, 1_ L%>`^l) *' q by K1;
       set r = <%-x, 1_ L%>; set rr = <%-x, 1_ L%>`^l;
       len p > 0 by B1, C1, AXIOMS:22; then p is non-zero by lenNZ;
       then reconsider q as non-zero Polynomial of L by L1, LM1;
       len q > 0 by lenNZ; then
   M1: len q >= 0+1 by NAT_1:38;
      thus thesis proof 0.L <> 1_ L by VECTSP_1:def 21; then
           len r = 2 by POLYNOM5:41; then
       A2: len rr = l*2 -l+1 by POLYNOM5:24;
       B2: l*2 -l+1 = l+l-l+1 by XCMPLX_1:11 .= l+1 by XCMPLX_1:26;
       C2: len rr > 1 by A2, J1, G1, E1, B2, NAT_1:38;
       F2: len rr > 0 & len q > 0 by C2, M1, AXIOMS:22; then
           rr.(len rr -'1) <> 0.L & q.(len q -'1) <> 0.L by LC1; then
       F2a: rr.(len rr -'1) * q.(len q -'1) <> 0.L by VECTSP_2:def 5;
       per cases by M1, REAL_1:def 5;
       suppose S1: len q = 1;
       A3: len p = len rr + len q -1 by F2a, L1, POLYNOM4:13
                .= len rr by S1, XCMPLX_1:26;
        thus degree BRoots p
        = degree (BRoots rr) + degree BRoots q by L1, BR1a
       .= degree (BRoots rr) + 0 by S1, BR1b
       .= l by BR1c .= l+l-l by XCMPLX_1:26 .= 2*l - l by XCMPLX_1:11
       .= 2*l-l+1-1 by XCMPLX_1:26
       .= len p -' 1 by A3, A2, B1, C1a, SCMFSA_7:3;
       suppose S1: len q > 1;
       E2: len rr < k & len q < k by B1, C2, L1, S1, LM2;
       D2: degree BRoots rr = l+1 -' 1 &
           degree BRoots q = len q -' 1 by A2, B2, E2, A1, F2;
      thus degree BRoots p
         = degree (BRoots rr) + degree BRoots q by L1, BR1a
        .= len rr-'1 + (len q -'1) by A2, B2, D2
        .= len rr-1 + (len q -'1) by C2, SCMFSA_7:3
        .= len rr-1 + (len q -1) by S1, SCMFSA_7:3
        .= len rr + (len q -1) -1 by XCMPLX_1:29
        .= len rr + (len q + -1) -1 by XCMPLX_0:def 8
        .= len rr + len q + -1 -1 by XCMPLX_1:1
        .= len rr + len q -1 -1 by XCMPLX_0:def 8
        .= len p -1 by F2a,L1, POLYNOM4:13 .= len p -' 1 by B1, C1, SCMFSA_7:3;
  end; end; end;
 for n being Nat holds P[n] from Comp_Ind(P);
 hence degree BRoots p = len p -' 1 by A;
end;

definition
  let L be add-associative right_zeroed right_complementable distributive
                                                (non empty doubleLoopStr),
      c be Element of L, n be Nat;
  func fpoly_mult_root(c,n) -> FinSequence of Polynom-Ring L means :LFPMR:
    len it = n &
    for i being Nat st i in dom it holds it.i = <% -c, 1_ L%>;
  existence proof
  <% -c, 1_ L%> is Element of Polynom-Ring L by POLYNOM3:def 12;
  then reconsider f = n |-> <% -c, 1_ L%>
     as FinSequence of Polynom-Ring L by FINSEQ_2:77;
   take f;
   thus
  A: len f = n by FINSEQ_2:69;
   let i be Nat;
   assume i in dom f; then i in Seg n by A, FINSEQ_1:def 3;
   hence f.i = <% -c, 1_ L%> by FINSEQ_2:70;
  end;
  uniqueness proof let it1, it2 be FinSequence of Polynom-Ring L such that
A1: len it1 = n and
B1: for i being Nat st i in dom it1 holds it1.i = <% -c, 1_ L%> and
A2: len it2 = n and
B2: for i being Nat st i in dom it2 holds it2.i = <% -c, 1_ L%>;
C: dom it1 = dom it2 by A1, A2, FINSEQ_3:31;
    now let x be Nat; assume
    D: x in dom it1;
     thus it1.x = <% -c, 1_ L%> by D, B1 .= it2.x by D, C, B2;
    end;
   hence it1 = it2 by C, FINSEQ_1:17;
  end;
end;

definition
  let L be add-associative right_zeroed right_complementable distributive
                                                (non empty doubleLoopStr),
      b be bag of the carrier of L;
  func poly_with_roots(b) -> Polynomial of L means                       :LPWR:
 ex f being FinSequence of (the carrier of Polynom-Ring L)*,
    s being FinSequence of L
  st len f = card support b & s = canFS(support b) & 
     (for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i)))
   & it = Product FlattenSeq f;
  existence proof
AA: support b c= dom b & dom b = the carrier of L by POLYNOM1:41, PBOOLE:def 3;
   rng canFS(support b) c= support b by FINSEQ_1:def 4; then
   rng canFS(support b) c= the carrier of L  by AA, XBOOLE_1:1; then
   reconsider s = canFS(support b) as FinSequence of L by FINSEQ_1:def 4;
   deffunc F(set) = fpoly_mult_root(s/.$1,b.(s/.$1));
   consider f being FinSequence such that
A: len f = card support b and
B: for k being Nat st k in Seg card support b holds f.k = F(k) from SeqLambda;
   rng f c= (the carrier of Polynom-Ring L)* proof let x be set;
     assume x in rng f; then consider i being Nat such that
   A1: i in dom f and
   B1: f.i = x by FINSEQ_2:11;
       i in Seg card support b by A1, A, FINSEQ_1:def 3; then
       x = F(i) by B1, B;
    hence x in (the carrier of Polynom-Ring L)* by FINSEQ_1:def 11;
   end; then
   reconsider f as FinSequence of (the carrier of Polynom-Ring L)*
       by FINSEQ_1:def 4;
   reconsider it1 = Product FlattenSeq f as Polynomial of L by POLYNOM3:def 12;
   take it1, f, s;
   thus len f = card support b by A;
   thus s = canFS(support b);
   hereby let i be Nat; assume i in dom f; then
       i in Seg card support b by A, FINSEQ_1:def 3;
     hence f.i = fpoly_mult_root(s/.i,b.(s/.i)) by B;
   end;
   thus thesis;
  end;
  uniqueness proof let it1, it2 be Polynomial of L;
    given f1 being FinSequence of (the carrier of Polynom-Ring L)*,
          s1 being FinSequence of L such that
A: len f1 = card support b & s1 = canFS(support b) & 
     (for i being Nat st i in dom f1
       holds f1.i = fpoly_mult_root(s1/.i,b.(s1/.i)))
   & it1 = Product FlattenSeq f1;
    given f2 being FinSequence of (the carrier of Polynom-Ring L)*,
          s2 being FinSequence of L such that
B: len f2 = card support b & s2 = canFS(support b) & 
     (for i being Nat st i in dom f2
       holds f2.i = fpoly_mult_root(s2/.i,b.(s2/.i)))
   & it2 = Product FlattenSeq f2;
C: dom f1 = dom f2 by A, B, FINSEQ_3:31;
D: dom f1 = Seg len f1 by FINSEQ_1:def 3;
   now let i be Nat; assume
   A1: i in Seg len f1;
    hence f1.i = fpoly_mult_root(s1/.i,b.(s1/.i)) by D, A
              .= f2.i by A, C, A1, D, B;
   end; then f1 = f2 by A, B, FINSEQ_2:10;
   hence thesis by A, B;
  end;
end;

theorem poly1: :: poly1:
for L being Abelian add-associative right_zeroed right_complementable
            commutative distributive right_unital (non empty doubleLoopStr)
 holds poly_with_roots(EmptyBag the carrier of L) = <%1_ L%>
proof let L be Abelian add-associative right_zeroed right_complementable
               commutative distributive right_unital (non empty doubleLoopStr);
 set b = EmptyBag the carrier of L;
 consider f being FinSequence of (the carrier of Polynom-Ring L)*,
         s being FinSequence of L such that
A: len f = card support b and s = canFS(support b) and
   for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))and
D: poly_with_roots(b) = Product FlattenSeq f by LPWR;
   card support b = 0 by CARD_1:78, BAGORDER:19; then
   f = <*>((the carrier of Polynom-Ring L)*) by A, FINSEQ_1:32; then
   FlattenSeq f = <*>(the carrier of Polynom-Ring L) by SCMFSA_7:13; then
   Product FlattenSeq f = 1_ Polynom-Ring L by FVSUM_1:98
                       .= 1_.(L) by POLYNOM3:def 12;
 hence thesis by D, poly1b;
end;

theorem poly1_1: :: poly1_1:
for L being add-associative right_zeroed right_complementable distributive
                                                 (non empty doubleLoopStr),
    c being Element of L
  holds poly_with_roots(({c},1)-bag) = <% -c, 1_ L %>
proof let L be add-associative right_zeroed right_complementable distributive
                                                 (non empty doubleLoopStr),
          c being Element of L;
  set b = ({c},1)-bag;
   consider f being FinSequence of (the carrier of Polynom-Ring L)*,
         s being FinSequence of L such that
A: len f = card support b and
B: s = canFS(support b) and
C: for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i))and
D: poly_with_roots(b) = Product FlattenSeq f by LPWR;
Da: support b = {c} by Snbagsup; then
E: card support b = 1 by CARD_1:79; then
F: f = <*f/.1*> by A, FINSEQ_5:15;
G: 1 in dom f by A, E, FINSEQ_3:27; then  f.1 = f/.1 by FINSEQ_4:def 4; then
Ia: FlattenSeq f = f.1 by F, DTCONSTR:13;
I: f.1 =  fpoly_mult_root(s/.1,b.(s/.1))  by G, C;
   set f1 = fpoly_mult_root(s/.1,b.(s/.1));
Ic: s = <* c *> by Da, B, CFS2;  len s = 1 by B, E, LCFS; then
    1 in dom s by FINSEQ_3:27; then
Ib: s/.1 = s.1 by FINSEQ_4:def 4 .= c by Ic, FINSEQ_1:57;
    c in {c} by TARSKI:def 1; then b.(s/.1) = 1 by Ib, Snbag1; then
J: len f1 = 1 by LFPMR;
K: for i being Nat st i in dom f1 holds f1.i = <% -c, 1_ L%> by Ib, LFPMR;
L: f1 = <*f1/.1*> by J, FINSEQ_5:15;
M: 1 in dom f1 by J, FINSEQ_3:27;
  thus poly_with_roots(({c},1)-bag)     = Product FlattenSeq f by D
    .= f1/.1 by Ia, I, L, FVSUM_1:99   .= f1.1 by M, FINSEQ_4:def 4
    .= <% -c, 1_ L %> by K, M;
end;

theorem PWRBBa: :: PWRBBa:
for L being add-associative right_zeroed right_complementable distributive
                                                (non empty doubleLoopStr),
    b being bag of the carrier of L,
    f being FinSequence of (the carrier of Polynom-Ring L)*,
    s being FinSequence of L
 st len f = card support b & s = canFS(support b) & 
    (for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i)))
  holds len FlattenSeq f = degree b
proof let L be add-associative right_zeroed right_complementable distributive
                                                (non empty doubleLoopStr),
    b being bag of the carrier of L,
    f being FinSequence of (the carrier of Polynom-Ring L)*,
    s being FinSequence of L such that
A: len f = card support b and
B: s = canFS(support b) and
C: for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i));
   len s = card support b by B, LCFS; then
Aa: dom f = dom s by A, FINSEQ_3:31;
   reconsider Cf = Card f as FinSequence of NAT;
D: len FlattenSeq f = Sum Cf by POLYNOM1:30;
   consider g being FinSequence of NAT such that
E: degree b = Sum g and
F: g = b*canFS(support b) by LBAGDEG;
   now
   A1: rng s c= dom b proof let x be set; assume x in rng s; then
       A2: x in support b by B, CFS1;  support b c= dom b by POLYNOM1:41;
         hence x in dom b by A2;
       end;
    thus dom Card f = dom f by CARD_3:def 2
                   .= dom g by B, F, Aa, A1, RELAT_1:46;
     let i be Nat such that
   C1: i in dom Card f;
   D1: i in dom f by C1, CARD_3:def 2; then
       f.i = fpoly_mult_root(s/.i,b.(s/.i)) by C; then
   E1: len (f.i) = b.(s/.i) by LFPMR;
   F1: g.i = b.(s.i) by D1, Aa, F, B, FUNCT_1:23;
     thus Cf.i = Card (f.i) by D1, CARD_3:def 2
               .= g.i by F1, E1, D1, Aa, FINSEQ_4:def 4;
   end; then
   Card f = b*canFS(support b) by F, FINSEQ_1:17; 
 hence len FlattenSeq f = degree b by D, E, F;
end;

theorem PWRBBb: :: PWRBBb:
for L being add-associative right_zeroed right_complementable distributive
                                                (non empty doubleLoopStr),
    b being bag of the carrier of L,
    f being FinSequence of (the carrier of Polynom-Ring L)*,
    s being FinSequence of L,
    c being Element of L
 st len f = card support b & s = canFS(support b) &
    (for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i)))
  holds (c in support b implies card ((FlattenSeq f)"{<% -c, 1_ L%>}) = b.c) &
        (not c in support b implies card ((FlattenSeq f)"{<% -c, 1_ L%>}) = 0)
proof
 let L be add-associative right_zeroed right_complementable distributive
                                                (non empty doubleLoopStr),
     b be bag of the carrier of L,
     f be FinSequence of (the carrier of Polynom-Ring L)*,
     s be FinSequence of L,
     c be Element of L such that
A: len f = card support b and
B: s = canFS(support b) and
C: for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i));
   len f = len s by A, B, LCFS; then
Ab: dom f = dom s by FINSEQ_3:31;
Ac: s is one-to-one by B, CFS0;
  hereby assume c in support b; then    c in rng s by B, CFS1; then
     consider i being Nat such that
  A1: i in dom s and
  B1: s.i = c by FINSEQ_2:11;
  B1a: s/.i = c by A1, B1, FINSEQ_4:def 4; 
  C1: card (b.c) = b.c by CARD_1:66;
  D1: b.c = { k where k is Nat : k < b.c } by AXIOMS:30;
      set ff = FlattenSeq f;  set Y = ff"{<% -c, 1_ L%>};
      set X = { k where k is Nat : k < b.c };
      defpred P[set,Nat] means ex n being Nat st n = $1 &
                                $2 = (Sum Card(f|(i-'1)))+(1+n);
  UN: for x,y1,y2 being set st x in X & P[x,y1] & P[x,y2] holds y1 = y2;
  EX: for x being set st x in X ex y being set st P[x,y] proof
        let x be set; assume x in X; then consider k being Nat such that
      A2: x = k and k < b.c;
        take y = (Sum Card(f|(i-'1)))+(1+k);  thus P[x,y] by A2;
      end;
      consider g being Function such that
  E1: dom g = X and
  F1: for x being set st x in X holds P[x,g.x] from FuncEx(UN,EX);
  Z1: g is one-to-one proof let x1,x2 be set such that
      A2: x1 in dom g and
      B2: x2 in dom g and
      C2: g.x1 = g.x2;          consider n1 being Nat such that
      D2: n1 = x1 and
      E2: g.x1 = (Sum Card(f|(i-'1)))+(1+n1) by E1, A2, F1;
          consider n2 being Nat such that
      F2: n2 = x2 and
      G2: g.x2 = (Sum Card(f|(i-'1)))+(1+n2) by E1, B2, F1;
          1+n1 = 1+n2 by C2, E2, G2, XCMPLX_1:2;
       hence x1 = x2 by D2, F2, XCMPLX_1:2;
      end;
      now let y be set;
       hereby assume y in rng g; then consider x being set such that
       A2: x in dom g and
       B2: y = g.x by FUNCT_1:def 5;
           consider k being Nat such that
       C2: x = k and
       D2: k < b.c by A2, E1;
           consider n being Nat such that
       E2: n = x and
       F2: g.x = (Sum Card(f|(i-'1)))+(1+n) by A2, E1, F1;
       G2: f.i = fpoly_mult_root(s/.i,b.(s/.i)) by A1, Ab, C;
       G2b: 1 <= 1+n & 1+n <= b.c by E2, C2, D2, NAT_1:38,37;
           len (f.i) = b.c by B1a, G2, LFPMR; then
       G2a: 1+n in dom (f.i) by G2b, FINSEQ_3:27; then
       H2:(Sum Card (f|(i-'1))) + (1+n) in dom ff &
          (f.i).(1+n) = ff.((Sum Card (f|(i-'1))) + (1+n))
             by A1, Ab, POLYNOM1:33;
          (f.i).(1+n) = <% -c, 1_ L%> by G2, G2a, B1a, LFPMR; then
          (f.i).(1+n) in {<% -c, 1_ L%>} by TARSKI:def 1;
        hence y in Y by H2, B2, F2, FUNCT_1:def 13;
       end;
       assume y in Y; then
      A2: y in dom ff & ff.y in {<% -c, 1_ L%>} by FUNCT_1:def 13;
          reconsider yn = y as Nat by A2, FINSEQ_3:25;
          consider i1, j being Nat such that
      B2: i1 in dom f and
      C2: j in dom (f.i1) and
      D2: yn = (Sum Card (f|(i1-'1))) + j and
      E2: (f.i1).j = ff.yn by A2, POLYNOM1:32;
          j <> 0 by C2, FINSEQ_3:26; then consider j1 being Nat such that
      G2: j = j1 + 1 by NAT_1:22;
      C3: f.i1 = fpoly_mult_root(s/.i1,b.(s/.i1)) by B2, C;
              (f.i1).j = <%-s/.i1, 1_ L%> by C3, C2, LFPMR; then
          D3: <% -c, 1_ L%> = <%-s/.i1, 1_ L%> by E2, A2, TARSKI:def 1; 
             <% -c, 1_ L%>.0 = -c & <% -s/.i1,1_ L%>.0 = -s/.i1 by POLYNOM5:39;
              then  -c = -s/.i1 by D3; then
          E3: c = s/.i1 by RLVECT_1:31;
          F3: i1 in dom s by B2, Ab; then s/.i1 = s.i1 by FINSEQ_4:def 4; then
              s.i = s.i1 by E3, B1; then
      J2: i1 = i by F3, A1, Ac, FUNCT_1:def 8;
          len (f.i1) = b.c by C3, E3, LFPMR; then
          j <= b.c by C2, FINSEQ_3:27; then j1 < b.c by G2, NAT_1:38; then
      G2a: j1 in X; then consider n being Nat such that
      H2: n = j1 and
      I2: g.j1 = (Sum Card(f|(i-'1)))+(1+n) by F1;
          g.j1 = y by J2, I2, H2, G2, D2;
       hence y in rng g by G2a, E1, FUNCT_1:12;
      end; then
      rng g = Y by TARSKI:2; then X,Y are_equipotent by Z1, E1, WELLORD2:def 4;
   hence card ((FlattenSeq f)"{<% -c, 1_ L%>}) = b.c by C1, D1, CARD_1:21;
  end;
  assume that
D: not c in support b and
E: card ((FlattenSeq f)"{<% -c, 1_ L%>}) <> 0;
   (FlattenSeq f)"{<% -c, 1_ L%>} <> {} by E, CARD_1:78; then
   consider x being set such that
F: x in (FlattenSeq f)"{<% -c, 1_ L%>} by XBOOLE_0:def 1;
G: x in dom FlattenSeq f by F, FUNCT_1:def 13; then
   reconsider x as Nat by FINSEQ_3:25;
   consider i, j being Nat such that
I: i in dom f and
J: j in dom (f.i) and x = (Sum Card (f|(i-'1))) + j and
K: (f.i).j = (FlattenSeq f).x by G, POLYNOM1:32;
   (FlattenSeq f).x in {<% -c, 1_ L%>} by F, FUNCT_1:def 13; then
H: (FlattenSeq f).x  = <% -c, 1_ L%> by TARSKI:def 1;
   f.i = fpoly_mult_root(s/.i,b.(s/.i)) by C, I; then
L: (f.i).j = <% -s/.i, 1_ L%> by J, LFPMR;
   <% -c, 1_ L%>.0 = -c & <% -s/.i, 1_ L%>.0 = -s/.i by POLYNOM5:39; then
   -c = -s/.i by L, H, K; then
M: c = s/.i by RLVECT_1:31;   i in dom s by Ab, I; then
   s/.i = s.i & s.i in rng s by FINSEQ_4:def 4, FUNCT_1:12; then
   c in support b by B, CFS1, M;
  hence contradiction by D;
end;

theorem PWRBB: :: PWRBB:
for L being comRing
for b1,b2 being bag of the carrier of L holds
  poly_with_roots(b1+b2) = (poly_with_roots b1)*'(poly_with_roots b2)
proof let L be comRing, b1,b2 be bag of the carrier of L;
  set b = b1+b2;
  consider f being FinSequence of (the carrier of Polynom-Ring L)*,
           s being FinSequence of L such that
A: len f = card support b and
B: s = canFS(support b) and
C: for i being Nat st i in dom f holds f.i = fpoly_mult_root(s/.i,b.(s/.i)) and
D: poly_with_roots(b1+b2) = Product FlattenSeq f by LPWR;
   consider f1 being FinSequence of (the carrier of Polynom-Ring L)*,
           s1 being FinSequence of L such that
Aa: len f1 = card support b1 and
Ba: s1 = canFS(support b1) and
Ca: for i being Nat st i in dom f1
     holds f1.i = fpoly_mult_root(s1/.i,b1.(s1/.i)) and
Da: poly_with_roots(b1) = Product FlattenSeq f1 by LPWR;
    consider f2 being FinSequence of (the carrier of Polynom-Ring L)*,
           s2 being FinSequence of L such that
Ab: len f2 = card support b2 and
Bb: s2 = canFS(support b2) and
Cb: for i being Nat st i in dom f2
     holds f2.i = fpoly_mult_root(s2/.i,b2.(s2/.i)) and
Db: poly_with_roots(b2) = Product FlattenSeq f2 by LPWR;
    set ff = FlattenSeq f, ff1 = FlattenSeq f1, ff2 = FlattenSeq f2;
    set g = (FlattenSeq f1) ^ (FlattenSeq f2);
E:  support b = support b1 \/ support b2 by POLYNOM1:42;
F:  len ff = degree b by A, B, C, PWRBBa;
G:  len ff1 = degree b1 by Aa, Ba, Ca, PWRBBa;
H:  len ff2 = degree b2 by Ab, Bb, Cb, PWRBBa;
    len g = len ff1 + len ff2 by FINSEQ_1:35
         .= degree b1 + degree b2 by G, H .= degree b by BAGDEG2; then
I:  dom ff = dom g by F, FINSEQ_3:31;
J:  len s = card support b by B, LCFS;
    now let x be set;
      set ffx = ff"{x}, gx = g"{x};
      per cases;
      suppose x in rng ff; then consider k being Nat such that
      A1: k in dom ff and
      B1: ff.k = x by FINSEQ_2:11;
          consider i, j being Nat such that
      C1: i in dom f and
      D1: j in dom (f.i) and k = (Sum Card (f|(i-'1))) + j and
      F1: (f.i).j = ff.k by A1, POLYNOM1:32;
      G1: f.i = fpoly_mult_root(s/.i,b.(s/.i)) by C1, C;
      H1: (f.i).j = <% -s/.i, 1_ L %> by D1, G1, LFPMR;
          i in dom s by J, A, C1, FINSEQ_3:31; then
          s.i = s/.i & s.i in rng s by FINSEQ_4:def 4, FUNCT_1:12; then
      K1: s/.i in support b by B, CFS1; then
      L1: card (ff"{x}) = b.(s/.i) by H1, F1, B1, A, B, C, PWRBBb;
      M1: card (g"{x}) = card (ff1"{x}) + card (ff2"{x}) by FINSEQ_3:63;
       thus card (ff"{x}) = card (g"{x}) proof
        per cases by K1, E, XBOOLE_0:def 2;
        suppose A2: s/.i in support b1 & not s/.i in support b2; then
        B2: card(ff1"{x}) = b1.(s/.i) by H1, F1, B1, Aa, Ba, Ca, PWRBBb;
        C2: card(ff2"{x}) = 0 by A2, H1, F1, B1, Ab, Bb, Cb, PWRBBb;
         thus card (ff"{x}) = b.(s/.i) by L1
           .= b1.(s/.i) + b2.(s/.i) by POLYNOM1:def 5
           .= b1.(s/.i) + 0 by A2, POLYNOM1:def 7
           .= card(g"{x}) by B2, C2, M1;
        suppose A2: not s/.i in support b1 & s/.i in support b2; then
        B2: card(ff1"{x}) = 0 by H1, F1, B1, Aa, Ba, Ca, PWRBBb;
        C2: card(ff2"{x}) = b2.(s/.i) by A2, H1, F1, B1, Ab, Bb, Cb, PWRBBb;
         thus card (ff"{x}) = b.(s/.i) by L1
           .= b1.(s/.i) + b2.(s/.i) by POLYNOM1:def 5
           .= 0+b2.(s/.i) by A2, POLYNOM1:def 7
           .= card(g"{x}) by B2, C2, M1;
        suppose A2: s/.i in support b1 & s/.i in support b2;then
        B2: card(ff1"{x}) = b1.(s/.i) by H1, F1, B1, Aa, Ba, Ca, PWRBBb;
        C2: card(ff2"{x}) = b2.(s/.i) by A2, H1, F1, B1, Ab, Bb, Cb, PWRBBb;
         thus card (ff"{x}) = b.(s/.i) by L1
           .= b1.(s/.i) + b2.(s/.i) by POLYNOM1:def 5
           .= card(g"{x}) by B2, C2, M1;
       end;
      suppose A1: not x in rng ff; then
      B1: ff"{x} = {} by FUNCT_1:142;
          now assume x in rng g; then
          AA: x in (rng ff1 \/ rng ff2) by FINSEQ_1:44;
           per cases by AA, XBOOLE_0:def 2;
           suppose x in rng ff1; then consider k being Nat such that
          A2: k in dom ff1 and
          B2: ff1.k = x by FINSEQ_2:11; consider i, j being Nat such that
          C2: i in dom f1 and
          D2: j in dom (f1.i) and k = (Sum Card (f1|(i-'1))) + j and
          F2: (f1.i).j = ff1.k by A2, POLYNOM1:32;
          G2: f1.i = fpoly_mult_root(s1/.i,b1.(s1/.i)) by C2, Ca;
          H2: (f1.i).j = <% -s1/.i, 1_ L %> by D2, G2, LFPMR;
              len s1 = card support b1 by Ba, LCFS;
              then i in dom s1 by Aa, C2, FINSEQ_3:31; then
              s1.i = s1/.i & s1.i in rng s1 by FINSEQ_4:def 4, FUNCT_1:12; then
              s1/.i in support b1 by Ba, CFS1; then
          K2a: s1/.i in support b by E, XBOOLE_0:def 2; then
              s1/.i in rng s by B, CFS1; then consider l being Nat such that
          L2: l in dom s and
          M2: s.l = s1/.i by FINSEQ_2:11;
          N2: l in dom f by A, L2, J, FINSEQ_3:31; then
          O2: f.l = fpoly_mult_root(s/.l,b.(s/.l)) by C;
          O2a: s.l = s/.l by L2, FINSEQ_4:def 4;
              b.(s1/.i) <> 0 by K2a, POLYNOM1:def 7; then
              0 < b.(s1/.i) by NAT_1:19; then
          O2b: 0+1 <= b.(s1/.i) by NAT_1:38;
              len (f.l) = b.(s/.l) by O2, LFPMR; then
          P2: 1 in dom (f.l) by O2a, O2b, M2, FINSEQ_3:27; then
              (Sum Card (f|(l-'1))) + 1 in dom ff &
              (f.l).1 = ff.((Sum Card (f|(l-'1))) + 1) by N2, POLYNOM1:33; then
          Q2: (f.l).1 in rng ff by FUNCT_1:12;
              (f.l).1 = <% -s/.l, 1_ L %> by P2, O2, LFPMR; 
           hence contradiction by Q2, A1, M2, H2, F2, B2, O2a;
           suppose x in rng ff2; then consider k being Nat such that
          A2: k in dom ff2 and
          B2: ff2.k = x by FINSEQ_2:11;
              consider i, j being Nat such that
          C2: i in dom f2 and
          D2: j in dom (f2.i) and k = (Sum Card (f2|(i-'1))) + j and
          F2: (f2.i).j = ff2.k by A2, POLYNOM1:32;
          G2: f2.i = fpoly_mult_root(s2/.i,b2.(s2/.i)) by C2, Cb;
          H2: (f2.i).j = <% -s2/.i, 1_ L %> by D2, G2, LFPMR;
              len s2 = card support b2 by Bb, LCFS;
              then i in dom s2 by Ab, C2, FINSEQ_3:31; then
              s2.i = s2/.i & s2.i in rng s2 by FINSEQ_4:def 4, FUNCT_1:12; then
              s2/.i in support b2 by Bb, CFS1; then
          K2a: s2/.i in support b by E, XBOOLE_0:def 2; then
              s2/.i in rng s by B, CFS1; then 
              consider l being Nat such that
          L2: l in dom s and
          M2: s.l = s2/.i by FINSEQ_2:11;
          N2: l in dom f by A, L2, J, FINSEQ_3:31; then
          O2: f.l = fpoly_mult_root(s/.l,b.(s/.l)) by C;
          O2a: s.l = s/.l by L2, FINSEQ_4:def 4;
              b.(s2/.i) <> 0 by K2a, POLYNOM1:def 7; then
              0 < b.(s2/.i) by NAT_1:19; then
          O2b: 0+1 <= b.(s2/.i) by NAT_1:38;
              len (f.l) = b.(s/.l) by O2, LFPMR; then
          P2: 1 in dom (f.l) by O2a, O2b, M2, FINSEQ_3:27; then
              (Sum Card (f|(l-'1))) + 1 in dom ff &
              (f.l).1 = ff.((Sum Card (f|(l-'1))) + 1) by N2, POLYNOM1:33; then
          Q2: (f.l).1 in rng ff by FUNCT_1:12;
              (f.l).1 = <% -s/.l, 1_ L %> by P2, O2, LFPMR; 
           hence contradiction by Q2, A1, M2, H2, F2, B2, O2a;
          end; then
      C1: g"{x} = {} by FUNCT_1:142;
       thus card (ff"{x}) = card (g"{x}) by B1, C1;      
    end; then
    ff, g are_fiberwise_equipotent by RFINSEQ:def 1; then
    consider p being Permutation of dom FlattenSeq f such that
Z:  FlattenSeq f = ((FlattenSeq f1) ^ (FlattenSeq f2)) * p by I, RFINSEQ:17;
 thus poly_with_roots(b1+b2)
    = Product ((FlattenSeq f1) ^ (FlattenSeq f2)) by I, Z, D, Permprod
   .= (Product FlattenSeq f1) * (Product FlattenSeq f2) by FVSUM_1:101
   .= (poly_with_roots b1)*'(poly_with_roots b2) by Da, Db, POLYNOM3:def 12;
end;

theorem  :: PWRBR1
for L being algebraic-closed domRing, p being non-zero (Polynomial of L)
 st p.(len p-'1) = 1_ L holds p = poly_with_roots(BRoots(p))
proof let L be algebraic-closed domRing, p be non-zero (Polynomial of L);assume
B: p.(len p-'1) = 1_ L;
   len p > 0 by lenNZ; then
A: len p >= 0+1 by NAT_1:38;
   defpred P[Nat] means
    for p being non-zero Polynomial of L
     st len p = $1 & $1 >= 1 & p.(len p -'1) = 1_ L
      holds p = poly_with_roots(BRoots(p));
P1: P[1] proof let p be non-zero Polynomial of L such that
    A1: len p = 1 and 1 >= 1 and
    C1: p.(len p -'1) = 1_ L;
        degree BRoots p = 0 by A1, BR1b; then
    D1: BRoots p = EmptyBag the carrier of L by BAGDEG0;
        len p -'1 = 0 by A1, GOBOARD9:1;
     hence p = <%1_ L%> by A1, C1, ALGSEQ_1:def 6
           .= poly_with_roots(BRoots(p)) by D1, poly1;
    end;
PS: for n being Nat st n >= 1 & P[n] holds P[n+1] proof
     let n be Nat such that
    A1: n >= 1 and
    B1: P[n];
     let p being non-zero Polynomial of L such that
    C1: len p = n+1 and n+1 >= 1 and
    E1: p.(len p -'1) = 1_ L;
    C1a: n+1 > 1 by A1, NAT_1:38; then
        p is with_roots by C1, POLYNOM5:def 8; then
        consider x being Element of L such that
    F1: x is_a_root_of p by POLYNOM5:def 7;
        set q = poly_quotient(p,x); set r = <%-x,1_ L%>;
        x in Roots p by F1,POLYNOM5:def 9; then
        x is_a_root_of p by POLYNOM5:def 9; then
    G1: p = r*'q by BEZOUT;
         len p > 0 by C1a, C1, AXIOMS:22; then p is non-zero by lenNZ; then
         reconsider q as non-zero Polynomial of L by G1, LM1;
        BRoots r = ({x},1)-bag by BR1e; then
    H1: BRoots(p) = ({x},1)-bag + BRoots(q) by G1, BR1d;
        1_ L <> 0.L by VECTSP_1:def 21; then
    H1b: len r = 2 by POLYNOM5:41;
        n+1 > 0 by C1a, AXIOMS:22; then
        len q > 0 by lenNZ; then
        r.(len r -'1) <> 0.L & q.(len q -'1) <> 0.L by H1b, LC1; then
        r.(len r -'1) * q.(len q -'1) <> 0.L by VECTSP_2:def 5; then
        len p = 2 + len q - 1 by H1b, G1, POLYNOM4:13; then
        len p = len q + 2 - 1; then len p = len q + (1+1)- 1; then
        len p = len q + 1+1- 1 by XCMPLX_1:1; then
        len p = len q +1 by XCMPLX_1:26; then
    I1a: len q = n by C1, XCMPLX_1:2;
        q.(len q -'1) = 1_ L by G1, E1, LM3; then
    I1: q = poly_with_roots(BRoots(q)) by I1a, A1, B1;
        poly_with_roots(({x},1)-bag) = <%-x,1_ L%> by poly1_1;
     hence p = poly_with_roots(BRoots(p)) by H1, I1, G1, PWRBB;
    end;
   for n  being Nat st n >= 1 holds P[n] from Ind1(P1,PS);
 hence p = poly_with_roots(BRoots(p)) by A, B;
end;

theorem  
for L being comRing, s being non empty finite Subset of L,
    f being FinSequence of Polynom-Ring L
 st len f = card s &
    for i being Nat, c being Element of L
     st i in dom f & c = (canFS(s)).i holds f.i = <% -c, 1_ L %>
  holds poly_with_roots((s,1)-bag) = Product(f)
proof let L be comRing;
   set cL = the carrier of L;
   set cPRL = the carrier of Polynom-Ring L;
   let s be non empty finite Subset of cL, f be FinSequence of cPRL such that
A: len f = card s and
B: for i being Nat, c being Element of cL
     st i in dom f & c = (canFS(s)).i holds f.i = <% -c, 1_ L %>;
   set cs = canFS(s);
C: len cs = card s by LCFS;  card s <> 0 by GRAPH_5:5; then
   0 < card s by NAT_1:19; then
D: 0+1 <= len f by A, NAT_1:38;
   cs | Seg len f is FinSequence by FINSEQ_1:23; then
X: cs | Seg len f = cs by A, C, FINSEQ_2:23;
   f | Seg len f is FinSequence by FINSEQ_1:23; then
Y: f | Seg len f = f by FINSEQ_2:23;
U: rng cs = s by CFS1;
W: dom f = dom cs by A, C, FINSEQ_3:31;
   defpred P[Nat] means
       ex t being finite Subset of cL, g being FinSequence of cPRL
        st t = rng (cs | Seg $1) & g = f | Seg $1 &
           poly_with_roots((t,1)-bag) = Product(g);   
P1: P[1] proof reconsider cs_1 = cs | Seg 1 as FinSequence of s by FINSEQ_1:23;
      reconsider g = f | Seg 1 as FinSequence of cPRL by FINSEQ_1:23;
      set t = rng cs_1;
      consider s1 being Element of s such that
  A1: cs_1 = <* s1 *> by A, C, D, QC_LANG4:7;
  B1: 1 in Seg 1 by FINSEQ_1:3; 1 in dom cs by D, A, C, FINSEQ_3:27; then
      reconsider cs1 = cs.1 as Element of s by FINSEQ_2:13;
  C1: cs_1.1 = cs1 by B1, FUNCT_1:72;
      cs1 in cL; then reconsider cs1 = cs.1 as Element of cL;
      cs_1.1 = s1 by A1, FINSEQ_1:57; then
  T1: t = {cs1} by A1, C1, FINSEQ_1:56;
      reconsider t = {cs1} as finite Subset of cL;
      consider p1 being Element of cPRL such that
  D1: g = <* p1 *> by D, QC_LANG4:7;
  D1a: 1 in dom f by D, FINSEQ_3:27; then
      reconsider f1 = f.1 as Element of cPRL by FINSEQ_2:13;
  E1: g.1 = f1 by B1, FUNCT_1:72;
  F1: g.1 = p1 by D1, FINSEQ_1:57;
      take t, g; thus t = rng (cs | Seg 1) & g = f | Seg 1 by T1;
  G1: Product(g) = p1 by D1, FVSUM_1:99;
      f1 = <% -cs1, 1_ L %> by D1a, B;
     hence poly_with_roots((t,1)-bag) = Product(g) by poly1_1, G1, E1, F1;
    end;
PIH: for j being Nat st 1 <= j & j < len f holds P[j] implies P[j+1]
  proof let j be Nat such that
  A1: 1 <= j and
  B1: j < len f;
      reconsider cs_j = cs | Seg j as FinSequence of s by FINSEQ_1:23;
      reconsider cs_j1 = cs | Seg (j+1) as FinSequence of s by FINSEQ_1:23;
      given t being finite Subset of cL, g being FinSequence of cPRL
      such that
  D1: t = rng (cs | Seg j) and
  E1: g = f | Seg j and
  F1: poly_with_roots((t,1)-bag) = Product(g);   
      reconsider g1 = f | Seg (j+1) as FinSequence of cPRL by FINSEQ_1:23;
      set t1 = rng cs_j1;
  F1a: 1 <= j+1 & j+1 <= len f by A1, B1, NAT_1:38; then
  G1: j+1 in dom cs by A,C,FINSEQ_3:27; then cs.(j+1) in s by FINSEQ_2:13; then
      cs.(j+1) in cL; then reconsider csj1 = cs.(j+1) as Element of cL;
      Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:11; then
  H1: cs_j1 = cs_j \/ cs|{j+1} by RELAT_1:107;
      cs|{j+1} = (j+1) .--> csj1 by G1, FUNCT_7:6;
      then rng (cs|{j+1}) = {csj1} by CQC_LANG:5; then 
      M1: t1 = t \/ {csj1} by H1, D1, RELAT_1:26; then
      reconsider t1 as finite Subset of cL;
      take t1, g1; thus t1 = rng (cs | Seg (j+1)) & g1 = f | Seg (j+1);
      reconsider pt = poly_with_roots((t,1)-bag) as Polynomial of L;
      reconsider ept = pt as Element of cPRL by POLYNOM3:def 12;
      reconsider pj1 = poly_with_roots(({csj1},1)-bag) as Polynomial of L;
      reconsider epj1 =<% -csj1, 1_ L %> as Element of cPRL by POLYNOM3:def 12;
      consider l being Nat such that
  I1a: len f = j+1+l by F1a, NAT_1:28;
  I1: len g1 = j+1 by I1a, FINSEQ_3:59;      j <= j+1 by NAT_1:37; then
      Seg j c= Seg (j+1) by FINSEQ_1:7; then
  J1: g = g1 | Seg j by E1, RELAT_1:103; j+1 in Seg (j+1) by FINSEQ_1:6; then
      g1.(j+1) = f.(j+1) by FUNCT_1:72 .= <% -csj1, 1_ L %> by G1, W, B; then
  K1: g1 = g ^ <* <% -csj1, 1_ L %> *> by I1, J1, FINSEQ_3:61;
  L1: pj1 = epj1 by poly1_1;
      t misses {csj1} proof assume not thesis; then
         t /\ {csj1} <> {} by XBOOLE_0:def 7; then
          consider x being set such that
      A2: x in t /\ {csj1} by XBOOLE_0:def 1;
      B2: x in t & x in {csj1} by A2, XBOOLE_0:def 3; then
      C2: x = csj1 by TARSKI:def 1;
          consider i being set such that
      D2: i in dom (cs | Seg j) and
      E2: x = (cs | Seg j).i by B2, D1, FUNCT_1:def 5;
      F2: i in Seg j by D2, RELAT_1:86; then
          reconsider i as Nat;
      G2: 1 <= i & i <= j by F2, FINSEQ_1:3;
      H2: i < j+1 by G2, NAT_1:38;         x = cs.i by D2, E2, FUNCT_1:70;
       hence contradiction by A, C2,G2,H2,F1a,C,U,GRAPH_5:10;
      end; then
      (t1,1)-bag = (t,1)-bag + ({csj1},1)-bag by M1, Snbagsum; 
      hence poly_with_roots((t1,1)-bag) = pt *' pj1 by PWRBB
        .= ept * epj1 by L1, POLYNOM3:def 12  .= Product(g) * epj1 by F1
        .= Product(g1) by K1, FVSUM_1:100;  
     end;
Z: for i being Nat st 1 <= i & i <= len f holds P[i] from FinInd(P1,PIH);
  consider t being finite Subset of cL, g being FinSequence of cPRL such that
Z1: t = rng (cs | Seg len f) and
Z2: g = f | Seg len f and
Z4: poly_with_roots((t,1)-bag) = Product(g) by D, Z;
 thus poly_with_roots((s,1)-bag) = Product(f) by Z1, Z2, Z4, X, Y, U;
end;
  
theorem :: PolyEval1:  
for L being non trivial comRing, s being non empty finite Subset of L,
    x being Element of L, f being FinSequence of L
 st len f = card s &
    for i being Nat, c being Element of L
     st i in dom f & c = (canFS(s)).i holds f.i = eval(<% -c, 1_ L %>,x)
  holds eval(poly_with_roots((s,1)-bag),x) = Product(f)
proof let L be non trivial comRing;
   set cL = the carrier of L;
   set cPRL = the carrier of Polynom-Ring L;
   let s be non empty finite Subset of cL, x be Element of cL,
          f be FinSequence of L such that
A: len f = card s and
B: for i being Nat, c being Element of cL
     st i in dom f & c = (canFS(s)).i holds f.i = eval(<% -c, 1_ L %>,x);
   set cs = canFS(s);
C: len cs = card s by LCFS;
   card s <> 0 by GRAPH_5:5; then  0 < card s by NAT_1:19; then
D: 0+1 <= len f by A, NAT_1:38;
   cs | Seg len f is FinSequence by FINSEQ_1:23; then
X: cs | Seg len f = cs by A, C, FINSEQ_2:23;
   f | Seg len f is FinSequence by FINSEQ_1:23; then
Y: f | Seg len f = f by FINSEQ_2:23;
U: rng cs = s by CFS1;
W: dom f = dom cs by A, C, FINSEQ_3:31;
   defpred P[Nat] means
       ex t being finite Subset of cL, g being FinSequence of cL
        st t = rng (cs | Seg $1) & g = f | Seg $1 &
           eval(poly_with_roots((t,1)-bag),x) = Product(g);   
P1: P[1] proof
      reconsider cs_1 = cs | Seg 1 as FinSequence of s by FINSEQ_1:23;
      reconsider g = f | Seg 1 as FinSequence of cL by FINSEQ_1:23;
      set t = rng cs_1;
      consider s1 being Element of s such that
  A1: cs_1 = <* s1 *> by A, C, D, QC_LANG4:7;
  B1: 1 in Seg 1 by FINSEQ_1:3;
      1 in dom cs by D, A, C, FINSEQ_3:27; then
      reconsider cs1 = cs.1 as Element of s by FINSEQ_2:13;
  C1: cs_1.1 = cs1 by B1, FUNCT_1:72;
      cs1 in cL; then reconsider cs1 = cs.1 as Element of cL;
      cs_1.1 = s1 by A1, FINSEQ_1:57; then
  T1: t = {cs1} by A1, C1, FINSEQ_1:56;
      reconsider t = {cs1} as finite Subset of cL;
      consider p1 being Element of cL such that
  D1: g = <* p1 *> by D, QC_LANG4:7;
  D1a: 1 in dom f by D, FINSEQ_3:27; then
      reconsider f1 = f.1 as Element of cL by FINSEQ_2:13;
  E1: g.1 = f1 by B1, FUNCT_1:72;
  F1: g.1 = p1 by D1, FINSEQ_1:57;
      take t, g;      thus t = rng (cs | Seg 1) & g = f | Seg 1 by T1;
  G1: Product(g) = p1 by D1, FVSUM_1:99;
      f1 = eval(<% -cs1, 1_ L %>,x) by D1a, B;
     hence eval(poly_with_roots((t,1)-bag),x) = Product(g) by poly1_1,G1,E1,F1;
    end;
PIH: for j being Nat st 1 <= j & j < len f holds P[j] implies P[j+1]
  proof let j be Nat such that
  A1: 1 <= j and
  B1: j < len f;
      reconsider cs_j = cs | Seg j as FinSequence of s by FINSEQ_1:23;
      reconsider cs_j1 = cs | Seg (j+1) as FinSequence of s by FINSEQ_1:23;
      given t being finite Subset of cL, g being FinSequence of cL
      such that
  D1: t = rng (cs | Seg j) and
  E1: g = f | Seg j and
  F1: eval(poly_with_roots((t,1)-bag),x) = Product(g);   
      reconsider g1 = f | Seg (j+1) as FinSequence of cL by FINSEQ_1:23;
      set t1 = rng cs_j1;
  F1a: 1 <= j+1 & j+1 <= len f by A1, B1, NAT_1:38; then
  G1: j+1 in dom cs by A,C,FINSEQ_3:27; then cs.(j+1) in s by FINSEQ_2:13; then
      cs.(j+1) in cL; then      reconsider csj1 = cs.(j+1) as Element of cL;
      Seg (j+1) = Seg j \/ {j+1} by FINSEQ_1:11; then
  H1: cs_j1 = cs_j \/ cs|{j+1} by RELAT_1:107;
      cs|{j+1} = (j+1) .--> csj1 by G1, FUNCT_7:6;
      then rng (cs|{j+1}) = {csj1} by CQC_LANG:5; then 
      M1: t1 = t \/ {csj1} by H1, D1, RELAT_1:26; then
      reconsider t1 as finite Subset of cL;
      take t1, g1;      thus t1 = rng (cs | Seg (j+1)) & g1 = f | Seg (j+1);
      reconsider pt = poly_with_roots((t,1)-bag) as Polynomial of L;
      reconsider pj1 = poly_with_roots(({csj1},1)-bag) as Polynomial of L;
      reconsider epj1 = <% -csj1, 1_ L %> as Element of cPRL
        by POLYNOM3:def 12;
      consider l being Nat such that
  I1a: len f = j+1+l by F1a, NAT_1:28;
  I1: len g1 = j+1 by I1a, FINSEQ_3:59;
      j <= j+1 by NAT_1:37; then
      Seg j c= Seg (j+1) by FINSEQ_1:7; then
  J1: g = g1 | Seg j by E1, RELAT_1:103;
      j+1 in Seg (j+1) by FINSEQ_1:6; then
      g1.(j+1) = f.(j+1) by FUNCT_1:72
              .= eval(<% -csj1, 1_ L %>,x) by G1, W, B; then
  K1: g1 = g ^ <* eval(<% -csj1, 1_ L %>,x) *> by I1, J1, FINSEQ_3:61;
  L1: pj1 = <% -csj1, 1_ L %> by poly1_1;
      t misses {csj1} proof assume not thesis; then
         t /\ {csj1} <> {} by XBOOLE_0:def 7; then
          consider x being set such that
      A2: x in t /\ {csj1} by XBOOLE_0:def 1;
      B2: x in t & x in {csj1} by A2, XBOOLE_0:def 3; then
      C2: x = csj1 by TARSKI:def 1;
          consider i being set such that
      D2: i in dom (cs | Seg j) and
      E2: x = (cs | Seg j).i by B2, D1, FUNCT_1:def 5;
      F2: i in Seg j by D2, RELAT_1:86; then reconsider i as Nat;
      G2: 1 <= i & i <= j by F2, FINSEQ_1:3;
      H2: i < j+1 by G2, NAT_1:38;         x = cs.i by D2, E2, FUNCT_1:70;
       hence contradiction by A, C2,G2,H2,F1a,C,U,GRAPH_5:10;
      end; then
      (t1,1)-bag = (t,1)-bag + ({csj1},1)-bag by M1, Snbagsum; then
      poly_with_roots((t1,1)-bag) = pt *' pj1 by PWRBB;
      hence eval(poly_with_roots((t1,1)-bag),x)
          = eval(pt,x) * eval(pj1,x) by POLYNOM4:27
         .= Product(g) * eval(pj1,x) by F1
         .= Product(g1) by K1, L1, FVSUM_1:100;  
     end;
Z: for i being Nat st 1 <= i & i <= len f holds P[i] from FinInd(P1,PIH);
  consider t being finite Subset of cL, g being FinSequence of cL such that
Z1: t = rng (cs | Seg len f) and
Z2: g = f | Seg len f and
Z4: eval(poly_with_roots((t,1)-bag),x) = Product(g) by D, Z;
 thus eval(poly_with_roots((s,1)-bag),x) = Product(f) by Z1, Z2, Z4, X, Y, U;
end;

Back to top