polynom8.miz



    begin

    

     Lm1: for j be Integer holds j >= 0 or j = ( - 1) or j < ( - 1)

    proof

      let j be Integer;

      per cases ;

        suppose j >= 0 ;

        hence thesis;

      end;

        suppose

         A1: j < 0 ;

        then

        reconsider n = ( - j) as Element of NAT by INT_1: 3;

        n <> ( - 0 ) by A1;

        then n >= 1 by NAT_1: 14;

        then n > 1 or n = 1 by XXREAL_0: 1;

        then ( - 1) > ( - ( - j)) or ( - 1) = j by XREAL_1: 24;

        hence thesis;

      end;

    end;

    

     Lm2: for j be Integer holds j >= 1 or j = 0 or j < 0

    proof

      let j be Integer;

      j < 0 or j is Element of NAT & (j <> 0 or j = 0 ) by INT_1: 3;

      hence thesis by NAT_1: 14;

    end;

    theorem :: POLYNOM8:1

    

     Th1: for n be Nat, L be well-unital domRing-like non degenerated non empty doubleLoopStr, x be Element of L st x <> ( 0. L) holds (x |^ n) <> ( 0. L)

    proof

      let n be Nat;

      let L be well-unital domRing-like non degenerated non empty doubleLoopStr, x be Element of L;

      defpred P[ Nat] means (x |^ $1) <> ( 0. L);

      assume

       A1: x <> ( 0. L);

       A2:

      now

        let n be Nat;

        assume P[n];

        then ((x |^ n) * x) <> ( 0. L) by A1, VECTSP_2:def 1;

        hence P[(n + 1)] by GROUP_1:def 7;

      end;

      (x |^ 0 ) = ( 1_ L) by BINOM: 8;

      then

       A3: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A3, A2);

      hence thesis;

    end;

    registration

      cluster almost_left_invertible -> domRing-like for associative well-unital add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      coherence

      proof

        let L be associative well-unital add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

        assume

         A1: L is almost_left_invertible;

        for x,y be Element of L holds (x * y) = ( 0. L) implies x = ( 0. L) or y = ( 0. L)

        proof

          let x,y be Element of L;

          assume

           A2: (x * y) = ( 0. L);

          now

            assume that

             A3: x <> ( 0. L) and

             A4: y <> ( 0. L);

            consider xx be Element of L such that

             A5: (xx * x) = ( 1. L) by A1, A3;

            y = (( 1. L) * y)

            .= (xx * (x * y)) by A5, GROUP_1:def 3

            .= ( 0. L) by A2;

            hence contradiction by A4;

          end;

          hence thesis;

        end;

        hence thesis by VECTSP_2:def 1;

      end;

    end

    theorem :: POLYNOM8:2

    

     Th2: for L be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr, x,y be Element of L st x <> ( 0. L) & y <> ( 0. L) holds ((x * y) " ) = ((x " ) * (y " ))

    proof

      let L be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr;

      let x,y be Element of L;

      assume that

       A1: x <> ( 0. L) and

       A2: y <> ( 0. L);

      

       A3: (((x " ) * (y " )) * (x * y)) = ((((x " ) * (y " )) * y) * x) by GROUP_1:def 3

      .= (((x " ) * ((y " ) * y)) * x) by GROUP_1:def 3

      .= (((x " ) * ( 1. L)) * x) by A2, VECTSP_1:def 10

      .= ((x " ) * x)

      .= ( 1. L) by A1, VECTSP_1:def 10;

      (x * y) <> ( 0. L) by A1, A2, VECTSP_1: 12;

      hence thesis by A3, VECTSP_1:def 10;

    end;

    theorem :: POLYNOM8:3

    

     Th3: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, z,z1 be Element of L holds z <> ( 0. L) implies z1 = ((z1 * z) / z)

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, z,z1 be Element of L;

      assume

       A1: z <> ( 0. L);

      

      thus ((z1 * z) / z) = (z1 * (z * (z " ))) by GROUP_1:def 3

      .= (z1 * ( 1. L)) by A1, VECTSP_1:def 10

      .= z1;

    end;

    theorem :: POLYNOM8:4

    

     Th4: for L be left_zeroed right_zeroed add-associative right_complementable non empty doubleLoopStr, m be Element of NAT , s be FinSequence of L st ( len s) = m & for k be Element of NAT st 1 <= k & k <= m holds (s /. k) = ( 1. L) holds ( Sum s) = (m * ( 1. L))

    proof

      let L be left_zeroed right_zeroed add-associative right_complementable non empty doubleLoopStr, m be Element of NAT , s be FinSequence of L;

      assume

       A1: ( len s) = m & for k be Element of NAT st 1 <= k & k <= m holds (s /. k) = ( 1. L);

      defpred P[ Nat] means for s be FinSequence of L st ( len s) = $1 & for k be Element of NAT st 1 <= k & k <= $1 holds (s /. k) = ( 1. L) holds ( Sum s) = ($1 * ( 1. L));

      

       A2: for l be Nat st P[l] holds P[(l + 1)]

      proof

        let l be Nat;

        assume

         A3: for g be FinSequence of L st (( len g) = l & for k be Element of NAT st 1 <= k & k <= l holds (g /. k) = ( 1. L)) holds ( Sum g) = (l * ( 1. L));

        for s be FinSequence of L st ( len s) = (l + 1) & for k be Element of NAT st 1 <= k & k <= (l + 1) holds (s /. k) = ( 1. L) holds ( Sum s) = ((l + 1) * ( 1. L))

        proof

          ex G be FinSequence of L st (( dom G) = ( Seg l) & for k be Nat st k in ( Seg l) holds (G . k) = ( 1. L))

          proof

            defpred P[ Nat, set] means $2 = ( 1. L);

            

             A4: for n be Nat st n in ( Seg l) holds ex x be Element of L st P[n, x];

            ex G be FinSequence of L st ( dom G) = ( Seg l) & for nn be Nat st nn in ( Seg l) holds P[nn, (G . nn)] from FINSEQ_1:sch 5( A4);

            hence thesis;

          end;

          then

          consider g be FinSequence of L such that

           A5: ( dom g) = ( Seg l) and

           A6: for k be Nat st k in ( Seg l) holds (g . k) = ( 1. L);

          

           A7: l in NAT by ORDINAL1:def 12;

          then

           A8: ( len g) = l by A5, FINSEQ_1:def 3;

          

           A9: for k be Nat st 1 <= k & k <= l holds (g /. k) = ( 1. L)

          proof

            let k be Nat;

            assume

             A10: 1 <= k & k <= l;

            then

             A11: k in ( dom g) by A5;

            k in ( Seg l) by A10;

            

            then ( 1. L) = (g . k) by A6

            .= (g /. k) by A11, PARTFUN1:def 6;

            hence thesis;

          end;

          then

           A12: for k be Element of NAT st 1 <= k & k <= l holds (g /. k) = ( 1. L);

          ( dom <*( 1. L)*>) = ( Seg 1) by FINSEQ_1:def 8;

          then

           A13: ( len <*( 1. L)*>) = 1 by FINSEQ_1:def 3;

          let s be FinSequence of L;

          assume that

           A14: ( len s) = (l + 1) and

           A15: for k be Element of NAT st 1 <= k & k <= (l + 1) holds (s /. k) = ( 1. L);

          

           A16: ( dom s) = ( Seg (l + 1)) by A14, FINSEQ_1:def 3;

          

           A17: for k be Nat st k in ( dom s) holds (s . k) = ((g ^ <*( 1. L)*>) . k)

          proof

            

             A18: ( dom s) = ( Seg (l + 1)) by A14, FINSEQ_1:def 3;

            let k be Nat;

            

             A19: k in NAT by ORDINAL1:def 12;

            assume

             A20: k in ( dom s);

            per cases by A20, A18, FINSEQ_1: 1;

              suppose

               A21: 1 <= k & k <= l;

              then

               A22: k <= (l + 1) by NAT_1: 12;

              

               A23: k in ( dom g) by A5, A21;

              

              then ((g ^ <*( 1. L)*>) . k) = (g . k) by FINSEQ_1:def 7

              .= (g /. k) by A23, PARTFUN1:def 6

              .= ( 1. L) by A9, A21

              .= (s /. k) by A15, A19, A21, A22

              .= (s . k) by A20, PARTFUN1:def 6;

              hence thesis;

            end;

              suppose

               A24: l < k & k <= (l + 1);

              then (k - k) <= ((l + 1) - k) by XREAL_1: 9;

              then

              reconsider ii = (((l + 1) - k) + 1) as Element of NAT by INT_1: 3;

              (l + 1) <= k by A24, NAT_1: 13;

              then ( dom <*( 1. L)*>) = ( Seg 1) & ii = ((k - k) + 1) by A24, FINSEQ_1:def 8, XXREAL_0: 1;

              then

               A25: ii in ( dom <*( 1. L)*>);

              (l + 0 ) < (k + l) by A24, XREAL_1: 8;

              then (l + 1) <= (k + l) by NAT_1: 13;

              then

               A26: ((l + 1) - l) <= ((k + l) - l) by XREAL_1: 9;

              (l + 1) <= k by A24, NAT_1: 13;

              then

               A27: ii = ((k - k) + 1) by A24, XXREAL_0: 1;

              

              then ((g ^ <*( 1. L)*>) . k) = ((g ^ <*( 1. L)*>) . (( len g) + ii)) by A5, FINSEQ_1:def 3, A7

              .= ( <*( 1. L)*> . 1) by A25, A27, FINSEQ_1:def 7

              .= ( 1. L) by FINSEQ_1:def 8

              .= (s /. k) by A15, A19, A24, A26

              .= (s . k) by A20, PARTFUN1:def 6;

              hence thesis;

            end;

          end;

          ( dom (g ^ <*( 1. L)*>)) = ( Seg (( len g) + ( len <*( 1. L)*>))) by FINSEQ_1:def 7

          .= ( dom s) by A5, A13, A16, FINSEQ_1:def 3, A7;

          then s = (g ^ <*( 1. L)*>) by A17, FINSEQ_1: 13;

          

          then ( Sum s) = (( Sum g) + ( 1. L)) by FVSUM_1: 71

          .= ((l * ( 1. L)) + ( 1. L)) by A3, A8, A12

          .= ((l * ( 1. L)) + (1 * ( 1. L))) by BINOM: 13

          .= ((l + 1) * ( 1. L)) by BINOM: 15;

          hence thesis;

        end;

        hence thesis;

      end;

      for s be FinSequence of L st ( len s) = 0 & for k be Element of NAT st 1 <= k & k <= 0 holds (s /. k) = ( 1. L) holds ( Sum s) = ( 0 * ( 1. L))

      proof

        let s be FinSequence of L;

        assume that

         A28: ( len s) = 0 and for k be Element of NAT st 1 <= k & k <= 0 holds (s /. k) = ( 1. L);

        

         A29: ( <*> the carrier of L) is Element of ( 0 -tuples_on the carrier of L) by FINSEQ_2: 131;

        s = {} by A28;

        

        then ( Sum s) = ( Sum ( <*> the carrier of L))

        .= ( 0. L) by A29, FVSUM_1: 74

        .= ( 0 * ( 1. L)) by BINOM: 12;

        hence thesis;

      end;

      then

       A30: P[ 0 ];

      for l be Nat holds P[l] from NAT_1:sch 2( A30, A2);

      hence thesis by A1;

    end;

    theorem :: POLYNOM8:5

    

     Th5: for L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, s be FinSequence of L, q be Element of L st q <> ( 1. L) & for i be Nat st 1 <= i & i <= ( len s) holds (s . i) = (q |^ (i -' 1)) holds ( Sum s) = ((( 1. L) - (q |^ ( len s))) / (( 1. L) - q))

    proof

      let L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, s be FinSequence of L, q be Element of L;

      assume

       A1: q <> ( 1. L) & for i be Nat st 1 <= i & i <= ( len s) holds (s . i) = (q |^ (i -' 1));

      defpred P[ Nat] means for s be FinSequence of L st ( len s) = $1 holds for q be Element of L st q <> ( 1. L) & for i be Nat st 1 <= i & i <= ( len s) holds (s . i) = (q |^ (i -' 1)) holds ( Sum s) = ((( 1. L) - (q |^ ( len s))) / (( 1. L) - q));

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: P[k];

        now

          let s be FinSequence of L;

          set f = (s | ( Seg k));

          reconsider f as FinSequence by FINSEQ_1: 15;

          assume

           A4: ( len s) = (k + 1);

          then

           A5: 1 <= ( len s) by NAT_1: 12;

          then ( len s) in ( dom s) by FINSEQ_3: 25;

          then

           A6: (s /. ( len s)) = (s . ( len s)) by PARTFUN1:def 6;

          

           A7: k <= ( len s) by A4, NAT_1: 13;

          then

           A8: ( len f) = k by FINSEQ_1: 17;

          now

            let u be object;

            assume u in ( rng f);

            then

            consider x be object such that

             A9: x in ( dom f) and

             A10: (f . x) = u by FUNCT_1:def 3;

            reconsider x9 = x as Element of NAT by A9;

            x9 <= ( len f) by A9, FINSEQ_3: 25;

            then

             A11: x9 <= ( len s) by A4, A8, NAT_1: 12;

            1 <= x9 by A9, FINSEQ_3: 25;

            then

             A12: x in ( dom s) by A11, FINSEQ_3: 25;

            (f . x) = (s . x) by A9, FUNCT_1: 47

            .= (s /. x) by A12, PARTFUN1:def 6;

            hence u in the carrier of L by A10;

          end;

          then ( rng f) c= the carrier of L by TARSKI:def 3;

          then

          reconsider f as FinSequence of L by FINSEQ_1:def 4;

          

           A13: ( len s) = (( len f) + 1) by A4, A7, FINSEQ_1: 17;

          let q be Element of L;

          assume that

           A14: q <> ( 1. L) and

           A15: for i be Nat st 1 <= i & i <= ( len s) holds (s . i) = (q |^ (i -' 1));

           A16:

          now

            assume (( 1. L) - q) = ( 0. L);

            then ((( 1. L) - q) + q) = q by ALGSTR_1:def 2;

            then (( 1. L) + (( - q) + q)) = q by RLVECT_1:def 3;

            then (( 1. L) + ( 0. L)) = q by RLVECT_1: 5;

            hence contradiction by A14, RLVECT_1:def 4;

          end;

          (( len s) - 1) >= (1 - 1) by A5, XREAL_1: 9;

          

          then

           A17: (( len s) -' 1) = (( len s) - 1) by XREAL_0:def 2

          .= ((( len f) + 1) - 1) by A4, A7, FINSEQ_1: 17;

           A18:

          now

            let i be Nat;

            assume that

             A19: 1 <= i and

             A20: i <= ( len f);

            

             A21: i <= ( len s) by A4, A8, A20, NAT_1: 13;

            i in ( dom f) by A19, A20, FINSEQ_3: 25;

            

            hence (f . i) = (s . i) by FUNCT_1: 47

            .= (q |^ (i -' 1)) by A15, A19, A21;

          end;

          f = (s | ( dom f)) by A7, FINSEQ_1: 17;

          

          hence ( Sum s) = (( Sum f) + (s /. ( len s))) by A13, A6, RLVECT_1: 38

          .= (((( 1. L) - (q |^ ( len f))) / (( 1. L) - q)) + (s /. ( len s))) by A3, A14, A7, A18, FINSEQ_1: 17

          .= (((( 1. L) - (q |^ ( len f))) / (( 1. L) - q)) + (q |^ ( len f))) by A15, A5, A17, A6

          .= (((( 1. L) - (q |^ ( len f))) / (( 1. L) - q)) + (((q |^ ( len f)) * (( 1. L) - q)) / (( 1. L) - q))) by A16, Th3

          .= (((( 1. L) - (q |^ ( len f))) + ((q |^ ( len f)) * (( 1. L) - q))) / (( 1. L) - q)) by VECTSP_1:def 3

          .= (((( 1. L) - (q |^ ( len f))) + (((q |^ ( len f)) * ( 1. L)) + ((q |^ ( len f)) * ( - q)))) / (( 1. L) - q)) by VECTSP_1:def 2

          .= (((( 1. L) - (q |^ ( len f))) + ((q |^ ( len f)) + ((q |^ ( len f)) * ( - q)))) / (( 1. L) - q))

          .= ((( 1. L) + (( - (q |^ ( len f))) + ((q |^ ( len f)) + ((q |^ ( len f)) * ( - q))))) / (( 1. L) - q)) by RLVECT_1:def 3

          .= ((( 1. L) + ((( - (q |^ ( len f))) + (q |^ ( len f))) + ((q |^ ( len f)) * ( - q)))) / (( 1. L) - q)) by RLVECT_1:def 3

          .= ((( 1. L) + (( 0. L) + ((q |^ ( len f)) * ( - q)))) / (( 1. L) - q)) by RLVECT_1: 5

          .= ((( 1. L) + ((q |^ ( len f)) * ( - q))) / (( 1. L) - q)) by ALGSTR_1:def 2

          .= ((( 1. L) + ( - ((q |^ ( len f)) * q))) / (( 1. L) - q)) by VECTSP_1: 8

          .= ((( 1. L) - (q |^ ( len s))) / (( 1. L) - q)) by A13, GROUP_1:def 7;

        end;

        hence thesis;

      end;

      now

        let s be FinSequence of L;

        assume ( len s) = 0 ;

        then

         A22: s = ( <*> the carrier of L);

        let q be Element of L;

        assume that q <> ( 1. L) and for i be Nat st 1 <= i & i <= ( len s) holds (s . i) = (q |^ (i -' 1));

        

        thus ((( 1. L) - (q |^ 0 )) / (( 1. L) - q)) = ((( 1. L) - ( 1_ L)) / (( 1. L) - q)) by BINOM: 8

        .= (( 0. L) / (( 1. L) - q)) by RLVECT_1: 15

        .= ( 0. L)

        .= ( Sum s) by A22, RLVECT_1: 43;

      end;

      then

       A23: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A23, A2);

      hence thesis by A1;

    end;

    definition

      let L be well-unital non empty doubleLoopStr, m be Element of NAT ;

      :: POLYNOM8:def1

      func emb (m,L) -> Element of L equals (m * ( 1. L));

      coherence ;

    end

    theorem :: POLYNOM8:6

    

     Th6: for L be Field, m,n,k be Element of NAT st m > 0 & n > 0 holds for M1 be Matrix of m, n, L, M2 be Matrix of n, k, L holds ((( emb (m,L)) * M1) * M2) = (( emb (m,L)) * (M1 * M2))

    proof

      let L be Field;

      let m,n,k be Element of NAT ;

      assume that

       A1: m > 0 and

       A2: n > 0 ;

      let M1 be Matrix of m, n, L;

      let M2 be Matrix of n, k, L;

      

       A3: ( width M1) = n by A1, MATRIX_0: 23

      .= ( len M2) by A2, MATRIX_0: 23;

      

       A4: ( width (( emb (m,L)) * M1)) = ( width M1) by MATRIX_3:def 5

      .= n by A1, MATRIX_0: 23

      .= ( len M2) by A2, MATRIX_0: 23;

      

       A5: for i,j be Nat st [i, j] in ( Indices ((( emb (m,L)) * M1) * M2)) holds (((( emb (m,L)) * M1) * M2) * (i,j)) = ((( emb (m,L)) * (M1 * M2)) * (i,j))

      proof

        let i,j be Nat;

        

         A6: ( len M1) = ( len (M1 * M2)) by A3, MATRIX_3:def 4;

        ( len ((( emb (m,L)) * M1) * M2)) = ( len (( emb (m,L)) * M1)) by A4, MATRIX_3:def 4

        .= ( len M1) by MATRIX_3:def 5;

        

        then

         A7: ( dom ((( emb (m,L)) * M1) * M2)) = ( Seg ( len M1)) by FINSEQ_1:def 3

        .= ( dom (M1 * M2)) by A6, FINSEQ_1:def 3;

        ( Seg ( len (( emb (m,L)) * ( Line (M1,i))))) = ( dom (( emb (m,L)) * ( Line (M1,i)))) by FINSEQ_1:def 3

        .= ( dom ( Line (M1,i))) by POLYNOM1:def 1

        .= ( Seg ( len ( Line (M1,i)))) by FINSEQ_1:def 3;

        

        then

         A8: ( len (( emb (m,L)) * ( Line (M1,i)))) = ( len ( Line (M1,i))) by FINSEQ_1: 6

        .= ( width M1) by MATRIX_0:def 7;

        

         A9: ( len ( Line (M1,i))) = ( len M2) by A3, MATRIX_0:def 7

        .= ( len ( Col (M2,j))) by MATRIX_0:def 8;

        assume

         A10: [i, j] in ( Indices ((( emb (m,L)) * M1) * M2));

        

        then

         A11: (((( emb (m,L)) * M1) * M2) * (i,j)) = (( Line ((( emb (m,L)) * M1),i)) "*" ( Col (M2,j))) by A4, MATRIX_3:def 4

        .= ( Sum ( mlt (( Line ((( emb (m,L)) * M1),i)),( Col (M2,j))))) by FVSUM_1:def 9;

        ( len ( Line ((( emb (m,L)) * M1),i))) = ( width (( emb (m,L)) * M1)) by MATRIX_0:def 7

        .= ( width M1) by MATRIX_3:def 5;

        then ( dom ( Line ((( emb (m,L)) * M1),i))) = ( Seg ( width M1)) by FINSEQ_1:def 3;

        then

         A12: ( dom ( Line ((( emb (m,L)) * M1),i))) = ( dom (( emb (m,L)) * ( Line (M1,i)))) by A8, FINSEQ_1:def 3;

        for k be Nat st k in ( dom ( Line ((( emb (m,L)) * M1),i))) holds (( Line ((( emb (m,L)) * M1),i)) . k) = ((( emb (m,L)) * ( Line (M1,i))) . k)

        proof

          ( len (M1 * M2)) = ( len M1) by A3, MATRIX_3:def 4

          .= m by A1, MATRIX_0: 23;

          then

           A13: ( dom (M1 * M2)) = ( Seg m) by FINSEQ_1:def 3;

          

           A14: ( Indices M1) = [:( Seg m), ( Seg n):] & i in ( dom (M1 * M2)) by A1, A10, A7, MATRIX_0: 23, ZFMISC_1: 87;

          let k be Nat;

          assume

           A15: k in ( dom ( Line ((( emb (m,L)) * M1),i)));

          

           A16: ( len ( Line ((( emb (m,L)) * M1),i))) = ( width (( emb (m,L)) * M1)) by MATRIX_0:def 7

          .= ( width M1) by MATRIX_3:def 5;

          then

           A17: k in ( Seg ( width M1)) by A15, FINSEQ_1:def 3;

          ( len ( Line (M1,i))) = ( width M1) by MATRIX_0:def 7;

          then k in ( dom ( Line (M1,i))) by A17, FINSEQ_1:def 3;

          then (( Line (M1,i)) . k) = (( Line (M1,i)) /. k) by PARTFUN1:def 6;

          then

          reconsider a = (( Line (M1,i)) . k) as Element of L;

          

           A18: a = (M1 * (i,k)) by A17, MATRIX_0:def 7;

          k in ( Seg n) by A1, A17, MATRIX_0: 23;

          then [i, k] in ( Indices M1) by A14, A13, ZFMISC_1: 87;

          then

           A19: (( emb (m,L)) * a) = ((( emb (m,L)) * M1) * (i,k)) by A18, MATRIX_3:def 5;

          ( dom ( Line ((( emb (m,L)) * M1),i))) = ( Seg ( width M1)) by A16, FINSEQ_1:def 3;

          then

           A20: k in ( Seg ( width (( emb (m,L)) * M1))) by A15, MATRIX_3:def 5;

          ((( emb (m,L)) * ( Line (M1,i))) . k) = (( emb (m,L)) * a) by A12, A15, FVSUM_1: 50;

          hence thesis by A20, A19, MATRIX_0:def 7;

        end;

        then

         A21: ( Line ((( emb (m,L)) * M1),i)) = (( emb (m,L)) * ( Line (M1,i))) by A12, FINSEQ_1: 13;

        ( Seg ( len (( emb (m,L)) * ( Line (M1,i))))) = ( dom (( emb (m,L)) * ( Line (M1,i)))) by FINSEQ_1:def 3

        .= ( dom ( Line (M1,i))) by POLYNOM1:def 1

        .= ( Seg ( len ( Line (M1,i)))) by FINSEQ_1:def 3;

        

        then

         A22: ( len (( emb (m,L)) * ( Line (M1,i)))) = ( len ( Line (M1,i))) by FINSEQ_1: 6

        .= ( len M2) by A3, MATRIX_0:def 7

        .= ( len ( Col (M2,j))) by MATRIX_0:def 8;

        

         A23: ( dom (( emb (m,L)) * ( Line (M1,i)))) = ( Seg ( len (( emb (m,L)) * ( Line (M1,i))))) by FINSEQ_1:def 3

        .= ( Seg ( len ( mlt ((( emb (m,L)) * ( Line (M1,i))),( Col (M2,j)))))) by A22, MATRIX_3: 6

        .= ( dom ( mlt ((( emb (m,L)) * ( Line (M1,i))),( Col (M2,j))))) by FINSEQ_1:def 3;

        

         A24: ( dom (( emb (m,L)) * ( Line (M1,i)))) = ( dom ( Line (M1,i))) by POLYNOM1:def 1

        .= ( Seg ( len ( Line (M1,i)))) by FINSEQ_1:def 3

        .= ( Seg ( len ( mlt (( Line (M1,i)),( Col (M2,j)))))) by A9, MATRIX_3: 6

        .= ( dom ( mlt (( Line (M1,i)),( Col (M2,j))))) by FINSEQ_1:def 3;

        then

         A25: ( dom ( mlt ((( emb (m,L)) * ( Line (M1,i))),( Col (M2,j))))) = ( dom (( emb (m,L)) * ( mlt (( Line (M1,i)),( Col (M2,j)))))) by A23, POLYNOM1:def 1;

        for k be Nat st k in ( dom ( mlt ((( emb (m,L)) * ( Line (M1,i))),( Col (M2,j))))) holds (( mlt ((( emb (m,L)) * ( Line (M1,i))),( Col (M2,j)))) . k) = ((( emb (m,L)) * ( mlt (( Line (M1,i)),( Col (M2,j))))) . k)

        proof

          

           A26: ( len ( Line (M1,i))) = ( len M2) by A3, MATRIX_0:def 7

          .= ( len ( Col (M2,j))) by MATRIX_0:def 8;

          

           A27: ( len ( Line (M1,i))) = ( width M1) by MATRIX_0:def 7;

          let k be Nat;

          assume

           A28: k in ( dom ( mlt ((( emb (m,L)) * ( Line (M1,i))),( Col (M2,j)))));

          ( dom ( Line (M1,i))) = ( Seg ( len ( Line (M1,i)))) by FINSEQ_1:def 3

          .= ( Seg ( len ( mlt (( Line (M1,i)),( Col (M2,j)))))) by A26, MATRIX_3: 6

          .= ( dom ( mlt (( Line (M1,i)),( Col (M2,j))))) by FINSEQ_1:def 3;

          then

           A29: k in ( Seg ( width M1)) by A23, A24, A28, A27, FINSEQ_1:def 3;

          then k in ( dom M2) by A3, FINSEQ_1:def 3;

          then

           A30: (( Col (M2,j)) . k) = (M2 * (k,j)) by MATRIX_0:def 8;

          (( Line (M1,i)) . k) = (M1 * (i,k)) by A29, MATRIX_0:def 7;

          then

          reconsider c = (( Col (M2,j)) . k), d = (( Line (M1,i)) . k) as Element of L by A30;

          (( mlt (( Line (M1,i)),( Col (M2,j)))) . k) = (c * d) by A23, A24, A28, FVSUM_1: 60;

          then

          reconsider a = (( mlt (( Line (M1,i)),( Col (M2,j)))) . k) as Element of L;

          

           A31: ((( emb (m,L)) * ( mlt (( Line (M1,i)),( Col (M2,j))))) . k) = (( emb (m,L)) * a) by A25, A28, FVSUM_1: 50;

          ((( emb (m,L)) * ( Line (M1,i))) . k) = (( emb (m,L)) * d) by A23, A28, FVSUM_1: 50;

          then

          reconsider b = ((( emb (m,L)) * ( Line (M1,i))) . k) as Element of L;

          (b * c) = ((( emb (m,L)) * d) * c) by A23, A28, FVSUM_1: 50

          .= (( emb (m,L)) * (d * c)) by GROUP_1:def 3

          .= (( emb (m,L)) * a) by A23, A24, A28, FVSUM_1: 60;

          hence thesis by A28, A31, FVSUM_1: 60;

        end;

        then

         A32: (( emb (m,L)) * ( mlt (( Line (M1,i)),( Col (M2,j))))) = ( mlt (( Line ((( emb (m,L)) * M1),i)),( Col (M2,j)))) by A21, A25, FINSEQ_1: 13;

        ( Seg ( width ((( emb (m,L)) * M1) * M2))) = ( Seg ( width M2)) by A4, MATRIX_3:def 4

        .= ( Seg ( width (M1 * M2))) by A3, MATRIX_3:def 4;

        then

         A33: [i, j] in ( Indices (M1 * M2)) by A10, A7;

        

        then ((( emb (m,L)) * (M1 * M2)) * (i,j)) = (( emb (m,L)) * ((M1 * M2) * (i,j))) by MATRIX_3:def 5

        .= (( emb (m,L)) * (( Line (M1,i)) "*" ( Col (M2,j)))) by A3, A33, MATRIX_3:def 4

        .= (( emb (m,L)) * ( Sum ( mlt (( Line (M1,i)),( Col (M2,j)))))) by FVSUM_1:def 9;

        hence thesis by A11, A32, FVSUM_1: 73;

      end;

      

       A34: ( len (( emb (m,L)) * (M1 * M2))) = ( len (M1 * M2)) by MATRIX_3:def 5

      .= ( len M1) by A3, MATRIX_3:def 4;

      ( width (( emb (m,L)) * (M1 * M2))) = ( width (M1 * M2)) by MATRIX_3:def 5

      .= ( width M2) by A3, MATRIX_3:def 4;

      then

       A35: ( width ((( emb (m,L)) * M1) * M2)) = ( width (( emb (m,L)) * (M1 * M2))) by A4, MATRIX_3:def 4;

      ( len ((( emb (m,L)) * M1) * M2)) = ( len (( emb (m,L)) * M1)) by A4, MATRIX_3:def 4

      .= ( len M1) by MATRIX_3:def 5;

      hence thesis by A34, A35, A5, MATRIX_0: 21;

    end;

    theorem :: POLYNOM8:7

    

     Th7: for L be non empty ZeroStr, p be AlgSequence of L, i be Element of NAT holds (p . i) <> ( 0. L) implies ( len p) >= (i + 1)

    proof

      let L be non empty ZeroStr, p be AlgSequence of L, i be Element of NAT ;

      

       A1: ( len p) is_at_least_length_of p by ALGSEQ_1:def 3;

      assume (p . i) <> ( 0. L);

      then ( len p) > i by A1, ALGSEQ_1:def 2;

      hence thesis by NAT_1: 13;

    end;

    theorem :: POLYNOM8:8

    

     Th8: for L be non empty ZeroStr, s be AlgSequence of L holds ( len s) > 0 implies (s . (( len s) - 1)) <> ( 0. L)

    proof

      let L be non empty ZeroStr, s be AlgSequence of L;

      assume ( len s) > 0 ;

      then ( len s) >= ( 0 + 1) by NAT_1: 13;

      then (( len s) - 1) >= (1 - 1) by XREAL_1: 9;

      then

      reconsider l = (( len s) - 1) as Element of NAT by INT_1: 3;

      assume

       A1: (s . (( len s) - 1)) = ( 0. L);

      now

        let i be Nat;

        assume

         A2: i >= l;

        per cases by A2, XXREAL_0: 1;

          suppose i = l;

          hence (s . i) = ( 0. L) by A1;

        end;

          suppose i > l;

          then i >= (l + 1) by NAT_1: 13;

          hence (s . i) = ( 0. L) by ALGSEQ_1: 8;

        end;

      end;

      then

       A3: l is_at_least_length_of s by ALGSEQ_1:def 2;

      ( len s) < (( len s) + 1) by NAT_1: 13;

      then (( len s) - 1) < ((( len s) + 1) - 1) by XREAL_1: 9;

      hence contradiction by A3, ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM8:9

    

     Th9: for L be add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr, p,q be Polynomial of L st ( len p) > 0 & ( len q) > 0 holds ( len (p *' q)) <= (( len p) + ( len q))

    proof

      let L be add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr;

      let p,q be Polynomial of L;

      assume that

       A1: ( len p) > 0 and

       A2: ( len q) > 0 ;

      

       A3: ((( len p) + ( len q)) - 1) <= ((( len p) + ( len q)) - 0 ) by XREAL_1: 13;

      (( len q) + 1) > ( 0 + 1) by A2, XREAL_1: 6;

      then ( len q) >= 1 by NAT_1: 13;

      then

       A4: (( len q) - 1) >= (1 - 1) by XREAL_1: 13;

      (q . (( len q) - 1)) <> ( 0. L) by A2, Th8;

      then

       A5: (q . (( len q) -' 1)) <> ( 0. L) by A4, XREAL_0:def 2;

      (( len p) + 1) > ( 0 + 1) by A1, XREAL_1: 6;

      then ( len p) >= 1 by NAT_1: 13;

      then

       A6: (( len p) - 1) >= (1 - 1) by XREAL_1: 13;

      (p . (( len p) - 1)) <> ( 0. L) by A1, Th8;

      then (p . (( len p) -' 1)) <> ( 0. L) by A6, XREAL_0:def 2;

      then ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) <> ( 0. L) by A5, VECTSP_2:def 1;

      hence thesis by A3, POLYNOM4: 10;

    end;

    theorem :: POLYNOM8:10

    

     Th10: for L be associative non empty doubleLoopStr, k,l be Element of L, seq be sequence of L holds (k * (l * seq)) = ((k * l) * seq)

    proof

      let L be associative non empty doubleLoopStr, k,l be Element of L, seq be sequence of L;

      now

        let i be Element of NAT ;

        

        thus ((k * (l * seq)) . i) = (k * ((l * seq) . i)) by POLYNOM5:def 4

        .= (k * (l * (seq . i))) by POLYNOM5:def 4

        .= ((k * l) * (seq . i)) by GROUP_1:def 3

        .= (((k * l) * seq) . i) by POLYNOM5:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    definition

      ::$Canceled

    end

    registration

      let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr;

      let m1,m2 be AlgSequence of L;

      cluster (m1 * m2) -> finite-Support;

      coherence

      proof

        set f = (m1 * m2);

        ex n be Nat st for i be Nat st i >= n holds (f . i) = ( 0. L)

        proof

          take (( len m1) + 1);

          now

            let i be Nat;

            assume i >= (( len m1) + 1);

            then i > ( len m1) by NAT_1: 13;

            then (m1 . i) = ( 0. L) by ALGSEQ_1: 8;

            

            hence ( 0. L) = ((m1 . i) * (m2 . i))

            .= (f . i) by LOPBAN_3:def 7;

          end;

          hence thesis;

        end;

        hence thesis by ALGSEQ_1:def 1;

      end;

    end

    theorem :: POLYNOM8:11

    

     Th11: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, m1,m2 be AlgSequence of L holds ( len (m1 * m2)) <= ( min (( len m1),( len m2)))

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, m1,m2 be AlgSequence of L;

      set p = (m1 * m2), k = ( min (( len m1),( len m2)));

      reconsider k as Element of NAT ;

      now

        let i be Nat;

        assume

         A1: i >= k;

        per cases by XXREAL_0: 15;

          suppose k = ( len m1);

          then (m1 . i) = ( 0. L) by A1, ALGSEQ_1: 8;

          

          hence ( 0. L) = ((m1 . i) * (m2 . i))

          .= (p . i) by LOPBAN_3:def 7;

        end;

          suppose k = ( len m2);

          then (m2 . i) = ( 0. L) by A1, ALGSEQ_1: 8;

          

          hence ( 0. L) = ((m1 . i) * (m2 . i))

          .= (p . i) by LOPBAN_3:def 7;

        end;

      end;

      then k is_at_least_length_of p by ALGSEQ_1:def 2;

      hence thesis by ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM8:12

    for L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, m1,m2 be AlgSequence of L st ( len m1) = ( len m2) holds ( len (m1 * m2)) = ( len m1)

    proof

      let L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, m1,m2 be AlgSequence of L;

      set p = (m1 * m2);

      assume

       A1: ( len m1) = ( len m2);

       A2:

      now

        per cases ;

          case ( len m1) = 0 ;

          hence ( len p) >= ( len m1);

        end;

          case ( len m1) <> 0 ;

          then ( len m1) >= ( 0 + 1) by NAT_1: 13;

          then (( len m1) - 1) >= (1 - 1) by XREAL_1: 9;

          then

          reconsider l = (( len m1) - 1) as Element of NAT by INT_1: 3;

          

           A3: (l + 1) = (( len m1) + 0 );

          then (m1 . l) <> ( 0. L) & (m2 . l) <> ( 0. L) by A1, ALGSEQ_1: 10;

          then ((m1 . l) * (m2 . l)) <> ( 0. L) by VECTSP_2:def 1;

          then (p . l) <> ( 0. L) by LOPBAN_3:def 7;

          hence ( len p) >= ( len m1) by A3, Th7;

        end;

      end;

      ( min (( len m1),( len m2))) = ( len m1) by A1;

      then ( len p) <= ( len m1) by Th11;

      hence thesis by A2, XXREAL_0: 1;

    end;

    begin

    definition

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, a be Element of L;

      let i be Integer;

      :: POLYNOM8:def3

      func pow (a,i) -> Element of L equals

      : Def2: (( power L) . (a,i)) if 0 <= i

      otherwise ((( power L) . (a, |.i.|)) " );

      coherence

      proof

         0 <= i implies (( power L) . (a,i)) is Element of L

        proof

          assume 0 <= i;

          then

          reconsider i9 = i as Element of NAT by INT_1: 3;

          (( power L) . (a,i9)) is Element of L;

          hence thesis;

        end;

        hence thesis;

      end;

      consistency ;

    end

    theorem :: POLYNOM8:13

    

     Th13: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L holds ( pow (x, 0 )) = ( 1. L)

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L;

      ( pow (x, 0 )) = (x |^ 0 ) by Def2

      .= ( 1_ L) by BINOM: 8;

      hence thesis;

    end;

    

     Lm3: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, a be Element of L, i be Integer holds 0 > i implies ( pow (a,i)) = (( pow (a, |.i.|)) " )

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, a be Element of L, i be Integer;

      assume

       A1: 0 > i;

      ( pow (a, |.i.|)) = (( power L) . (a, |.i.|)) by Def2;

      hence thesis by A1, Def2;

    end;

    

     Lm4: for L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, i be Integer, x be Element of L holds i <= 0 implies ( pow (x,i)) = (( pow (x, |.i.|)) " )

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr;

      let i be Integer;

      let x be Element of L;

      

       A1: ( 1. L) <> ( 0. L);

      assume

       A2: i <= 0 ;

      per cases by A2;

        suppose i < 0 ;

        hence thesis by Lm3;

      end;

        suppose

         A3: i = 0 ;

        

        hence ( pow (x,i)) = ( 1. L) by Th13

        .= (( 1. L) * (( 1. L) " )) by A1, VECTSP_1:def 10

        .= (( 1_ L) " )

        .= ((x |^ 0 ) " ) by BINOM: 8

        .= ((x |^ |.i.|) " ) by A3, ABSVALUE:def 1

        .= (( pow (x, |.i.|)) " ) by Def2;

      end;

    end;

    theorem :: POLYNOM8:14

    

     Th14: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L holds ( pow (x,1)) = x

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr;

      let x be Element of L;

      

      thus ( pow (x,1)) = (x |^ 1) by Def2

      .= x by BINOM: 8;

    end;

    theorem :: POLYNOM8:15

    

     Th15: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L holds ( pow (x,( - 1))) = (x " )

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L;

       |.( - 1).| = ( - ( - 1)) by ABSVALUE:def 1;

      

      hence ( pow (x,( - 1))) = (( pow (x,1)) " ) by Lm3

      .= (x " ) by Th14;

    end;

    

     Lm5: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, i be Element of NAT holds ( pow (( 1. L),i)) = ( 1. L)

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr;

      let i be Element of NAT ;

      defpred P[ Nat] means ( pow (( 1. L),$1)) = ( 1. L);

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        ( pow (( 1. L),(k + 1))) = (( power L) . (( 1. L),(k + 1))) by Def2

        .= ((( power L) . (( 1. L),k)) * ( 1. L)) by GROUP_1:def 7

        .= (( 1. L) * ( 1. L)) by A2, Def2

        .= ( 1. L);

        hence P[(k + 1)];

      end;

      ( pow (( 1_ L), 0 )) = (( power L) . (( 1. L), 0 )) by Def2;

      then

       A3: P[ 0 ] by GROUP_1:def 7;

      for k be Nat holds P[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: POLYNOM8:16

    

     Th16: for L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, i be Integer holds ( pow (( 1. L),i)) = ( 1. L)

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr;

      let i be Integer;

      per cases ;

        suppose 0 <= i;

        then i is Element of NAT by INT_1: 3;

        hence thesis by Lm5;

      end;

        suppose

         A1: 0 > i;

        

         A2: ( 1. L) <> ( 0. L) & (( 1. L) * ( 1. L)) = ( 1. L);

        

         A3: ( pow (( 1. L), |.i.|)) = ( 1. L) by Lm5;

        ( pow (( 1. L),i)) = ((( power L) . (( 1. L), |.i.|)) " ) by A1, Def2

        .= (( 1. L) " ) by A3, Def2;

        hence thesis by A2, VECTSP_1:def 10;

      end;

    end;

    theorem :: POLYNOM8:17

    

     Th17: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L, n be Element of NAT holds ( pow (x,(n + 1))) = (( pow (x,n)) * x) & ( pow (x,(n + 1))) = (x * ( pow (x,n)))

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr;

      let x be Element of L;

      let n be Element of NAT ;

      ( pow (x,(n + 1))) = (x |^ (n + 1)) by Def2

      .= ((x |^ n) * x) by GROUP_1:def 7

      .= (( pow (x,n)) * x) by Def2;

      hence thesis;

    end;

    

     Lm6: for L be well-unital non empty doubleLoopStr, n be Element of NAT holds (( 1. L) |^ n) = ( 1. L)

    proof

      let L be well-unital non empty doubleLoopStr, n be Element of NAT ;

      defpred P[ Nat] means (( 1. L) |^ $1) = ( 1_ L);

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        (( 1. L) |^ (k + 1)) = ((( 1. L) |^ k) * ( 1. L)) by GROUP_1:def 7

        .= ( 1. L) by A2;

        hence P[(k + 1)];

      end;

      

       A3: P[ 0 ] by BINOM: 8;

      for k be Nat holds P[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm7: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, m be Element of NAT , x be Element of L st x <> ( 0. L) holds ((x |^ m) * ((x " ) |^ m)) = ( 1. L)

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, m be Element of NAT , x be Element of L;

      assume

       A1: x <> ( 0. L);

      ((x |^ m) * ((x " ) |^ m)) = ((x * (x " )) |^ m) by BINOM: 9

      .= (( 1. L) |^ m) by A1, VECTSP_1:def 10

      .= ( 1. L) by Lm6;

      hence thesis;

    end;

    theorem :: POLYNOM8:18

    

     Th18: for L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, i be Integer, x be Element of L st x <> ( 0. L) holds (( pow (x,i)) " ) = ( pow (x,( - i)))

    proof

      let L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr;

      let i be Integer;

      let x be Element of L;

      assume

       A1: x <> ( 0. L);

      

       A2: ( 1. L) <> ( 0. L);

      per cases ;

        suppose

         A3: i >= 0 ;

        per cases by A3, XREAL_1: 24;

          suppose

           A4: ( - i) < ( - 0 );

          

          hence ( pow (x,( - i))) = (( pow (x, |.( - i).|)) " ) by Lm3

          .= (( pow (x,( - ( - i)))) " ) by A4, ABSVALUE:def 1

          .= (( pow (x,i)) " );

        end;

          suppose

           A5: i = 0 ;

          

          hence ( pow (x,( - i))) = ( 1. L) by Th13

          .= (( 1. L) * (( 1. L) " )) by A2, VECTSP_1:def 10

          .= (( 1. L) " )

          .= (( pow (x,i)) " ) by A5, Th13;

        end;

      end;

        suppose

         A6: i < 0 ;

        

         A7: ( pow (x, |.i.|)) = (x |^ |.i.|) by Def2;

        ( pow (x,i)) = (( pow (x, |.i.|)) " ) by A6, Lm3;

        then (( pow (x,i)) " ) = ( pow (x, |.i.|)) by A1, A7, Th1, VECTSP_1: 24;

        hence thesis by A6, ABSVALUE:def 1;

      end;

    end;

    theorem :: POLYNOM8:19

    

     Th19: for L be Field, j be Integer, x be Element of L st x <> ( 0. L) holds ( pow (x,(j + 1))) = (( pow (x,j)) * ( pow (x,1)))

    proof

      let L be Field;

      let j be Integer;

      let x be Element of L;

      

       A1: ( pow (x,( - 1))) = ((x |^ |.( - 1).|) " ) by Def2;

      assume

       A2: x <> ( 0. L);

      then (x |^ |.( - 1).|) <> ( 0. L) by Th1;

      then

       A3: ( pow (x,( - 1))) <> ( 0. L) by A1, VECTSP_1: 25;

      

       A4: ( pow (x,( - j))) <> ( 0. L)

      proof

        per cases ;

          suppose 0 <= ( - j);

          then

          reconsider k = ( - j) as Element of NAT by INT_1: 3;

          ( pow (x,( - j))) = (x |^ k) by Def2;

          hence thesis by A2, Th1;

        end;

          suppose

           A5: ( - j) < 0 ;

          

           A6: (x |^ |.( - j).|) <> ( 0. L) by A2, Th1;

          ( pow (x,( - j))) = ((x |^ |.( - j).|) " ) by A5, Def2;

          hence thesis by A6, VECTSP_1: 25;

        end;

      end;

      

       A7: ( pow (x,(j + 1))) <> ( 0. L)

      proof

        per cases ;

          suppose 0 <= (j + 1);

          then

          reconsider k = (j + 1) as Element of NAT by INT_1: 3;

          ( pow (x,(j + 1))) = (x |^ k) by Def2;

          hence thesis by A2, Th1;

        end;

          suppose

           A8: (j + 1) < 0 ;

          

           A9: (x |^ |.(j + 1).|) <> ( 0. L) by A2, Th1;

          ( pow (x,(j + 1))) = ((x |^ |.(j + 1).|) " ) by A8, Def2;

          hence thesis by A9, VECTSP_1: 25;

        end;

      end;

       A10:

      now

        per cases by Lm1;

          suppose

           A11: j >= 0 ;

          then

          reconsider n = j as Element of NAT by INT_1: 3;

          

           A12: (n + 1) = |.(j + 1).| by ABSVALUE:def 1;

          ( pow (x, |.j.|)) = (x |^ |.j.|) by Def2;

          then

           A13: ( pow (x, |.j.|)) <> ( 0. L) by A2, Th1;

          ( pow (x, |.(j + 1).|)) = (x |^ |.(j + 1).|) by Def2;

          then

           A14: ( pow (x, |.(j + 1).|)) <> ( 0. L) by A2, Th1;

          (n + 1) >= 0 ;

          

          hence (( pow (x,(j + 1))) * (( pow (x,( - 1))) * ( pow (x,( - j))))) = (( pow (x, |.(j + 1).|)) * (( pow (x,( - 1))) * ( pow (x,( - j))))) by ABSVALUE:def 1

          .= (( pow (x, |.(j + 1).|)) * ((x " ) * ( pow (x,( - j))))) by Th15

          .= (( pow (x, |.(j + 1).|)) * ((x " ) * (( pow (x,j)) " ))) by A2, Th18

          .= (( pow (x, |.(j + 1).|)) * ((x " ) * (( pow (x, |.j.|)) " ))) by A11, ABSVALUE:def 1

          .= (( pow (x, |.(j + 1).|)) * ((x * ( pow (x, |.j.|))) " )) by A2, A13, Th2

          .= (( pow (x, |.(j + 1).|)) * (( pow (x,( |.j.| + 1))) " )) by Th17

          .= (( pow (x, |.(j + 1).|)) * (( pow (x, |.(j + 1).|)) " )) by A12, ABSVALUE:def 1

          .= ( 1. L) by A14, VECTSP_1:def 10;

        end;

          suppose

           A15: j < ( - 1);

          

           A16: ( pow (x,( - j))) <> ( 0. L)

          proof

            reconsider k = ( - j) as Element of NAT by A15, INT_1: 3;

            ( pow (x,( - j))) = (x |^ k) by Def2;

            hence thesis by A2, Th1;

          end;

          ( pow (x, |.(j + 1).|)) = (x |^ |.(j + 1).|) by Def2;

          then

           A17: ( pow (x, |.(j + 1).|)) <> ( 0. L) by A2, Th1;

          

           A18: (j + 1) < (( - 1) + 1) by A15, XREAL_1: 6;

          

          hence (( pow (x,(j + 1))) * (( pow (x,( - 1))) * ( pow (x,( - j))))) = ((( pow (x, |.(j + 1).|)) " ) * (( pow (x,( - 1))) * ( pow (x,( - j))))) by Lm3

          .= ((( pow (x, |.(j + 1).|)) " ) * ((x " ) * ( pow (x,( - j))))) by Th15

          .= (((( pow (x, |.(j + 1).|)) " ) * (x " )) * ( pow (x,( - j)))) by GROUP_1:def 3

          .= (((( pow (x, |.(j + 1).|)) * x) " ) * ( pow (x,( - j)))) by A2, A17, Th2

          .= ((( pow (x,( |.(j + 1).| + 1))) " ) * ( pow (x,( - j)))) by Th17

          .= ((( pow (x,(( - (j + 1)) + 1))) " ) * ( pow (x,( - j)))) by A18, ABSVALUE:def 1

          .= ( 1. L) by A16, VECTSP_1:def 10;

        end;

          suppose

           A19: j = ( - 1);

          

           A20: (x " ) <> ( 0. L) by A2, VECTSP_1: 25;

          

          thus (( pow (x,(j + 1))) * (( pow (x,( - 1))) * ( pow (x,( - j))))) = (( 1. L) * (( pow (x,( - 1))) * ( pow (x,( - j))))) by A19, Th13

          .= (( pow (x,( - 1))) * ( pow (x,( - j))))

          .= ((x " ) * ( pow (x,( - j)))) by Th15

          .= ((x " ) * (( pow (x,j)) " )) by A2, Th18

          .= ((x " ) * ((x " ) " )) by A19, Th15

          .= ( 1. L) by A20, VECTSP_1:def 10;

        end;

      end;

      

       A21: ( pow (x,(j + 1))) <> ( 0. L)

      proof

        per cases ;

          suppose 0 <= (j + 1);

          then

          reconsider k = (j + 1) as Element of NAT by INT_1: 3;

          ( pow (x,(j + 1))) = (x |^ k) by Def2;

          hence thesis by A2, Th1;

        end;

          suppose

           A22: (j + 1) < 0 ;

          

           A23: (x |^ |.(j + 1).|) <> ( 0. L) by A2, Th1;

          ( pow (x,(j + 1))) = ((x |^ |.(j + 1).|) " ) by A22, Def2;

          hence thesis by A23, VECTSP_1: 25;

        end;

      end;

      (( pow (x,(j + 1))) * ( pow (x,( - (j + 1))))) = (( pow (x,(j + 1))) * (( pow (x,(j + 1))) " )) by A2, Th18

      .= ( 1. L) by A7, VECTSP_1:def 10;

      then

       A24: ( pow (x,( - (j + 1)))) = (( pow (x,( - 1))) * ( pow (x,( - j)))) by A10, A21, VECTSP_1: 5;

      

      thus ( pow (x,(j + 1))) = ( pow (x,( - ( - (j + 1)))))

      .= ((( pow (x,( - 1))) * ( pow (x,( - j)))) " ) by A2, A24, Th18

      .= ((( pow (x,( - j))) " ) * (( pow (x,( - 1))) " )) by A4, A3, Th2

      .= (( pow (x,( - ( - j)))) * (( pow (x,( - 1))) " )) by A2, Th18

      .= (( pow (x,j)) * ( pow (x,( - ( - 1))))) by A2, Th18

      .= (( pow (x,j)) * ( pow (x,1)));

    end;

    theorem :: POLYNOM8:20

    

     Th20: for L be Field, j be Integer, x be Element of L st x <> ( 0. L) holds ( pow (x,(j - 1))) = (( pow (x,j)) * ( pow (x,( - 1))))

    proof

      let L be Field;

      let j be Integer;

      let x be Element of L;

      assume

       A1: x <> ( 0. L);

      

       A2: ( pow (x,(j - 1))) <> ( 0. L)

      proof

        per cases ;

          suppose 0 <= (j - 1);

          then

          reconsider k = (j - 1) as Element of NAT by INT_1: 3;

          ( pow (x,(j - 1))) = (x |^ k) by Def2;

          hence thesis by A1, Th1;

        end;

          suppose

           A3: (j - 1) < 0 ;

          

           A4: (x |^ |.(j - 1).|) <> ( 0. L) by A1, Th1;

          ( pow (x,(j - 1))) = ((x |^ |.(j - 1).|) " ) by A3, Def2;

          hence thesis by A4, VECTSP_1: 25;

        end;

      end;

       A5:

      now

        per cases by Lm2;

          suppose

           A6: j >= 1;

          then

           A7: |.j.| = j by ABSVALUE:def 1;

          ( pow (x, |.( - j).|)) = (x |^ |.( - j).|) by Def2;

          then

           A8: ( pow (x, |.( - j).|)) <> ( 0. L) by A1, Th1;

          

           A9: |.j.| = |.( - j).| by COMPLEX1: 52;

          j >= (1 + 0 ) by A6;

          then

           A10: (j - 1) >= 0 by XREAL_1: 19;

          

          then

           A11: ( |.(j - 1).| + 1) = ((j - 1) + 1) by ABSVALUE:def 1

          .= j;

          

          thus (( pow (x,(j - 1))) * (x * ( pow (x,( - j))))) = ((( pow (x,(j - 1))) * x) * ( pow (x,( - j)))) by GROUP_1:def 3

          .= ((( pow (x, |.(j - 1).|)) * x) * ( pow (x,( - j)))) by A10, ABSVALUE:def 1

          .= ((( pow (x, |.(j - 1).|)) * x) * (( pow (x, |.( - j).|)) " )) by A6, Lm4

          .= (( pow (x,( |.(j - 1).| + 1))) * (( pow (x, |.( - j).|)) " )) by Th17

          .= ( 1. L) by A8, A11, A7, A9, VECTSP_1:def 10;

        end;

          suppose

           A12: j < 0 ;

          ( pow (x, |.(j - 1).|)) = (x |^ |.(j - 1).|) by Def2;

          then

           A13: ( pow (x, |.(j - 1).|)) <> ( 0. L) by A1, Th1;

          

           A14: (1 - j) = ( - (j - 1));

          

          thus (( pow (x,(j - 1))) * (x * ( pow (x,( - j))))) = ((( pow (x, |.(j - 1).|)) " ) * (x * ( pow (x,( - j))))) by A12, Lm3

          .= ((( pow (x, |.(j - 1).|)) " ) * (x * ( pow (x, |.( - j).|)))) by A12, ABSVALUE:def 1

          .= ((( pow (x, |.(j - 1).|)) " ) * ( pow (x,(1 + |.( - j).|)))) by Th17

          .= ((( pow (x, |.(j - 1).|)) " ) * ( pow (x,(1 + ( - j))))) by A12, ABSVALUE:def 1

          .= ((( pow (x, |.(j - 1).|)) " ) * ( pow (x, |.(j - 1).|))) by A12, A14, ABSVALUE:def 1

          .= ( 1. L) by A13, VECTSP_1:def 10;

        end;

          suppose

           A15: j = 0 ;

          

          hence (( pow (x,(j - 1))) * (x * ( pow (x,( - j))))) = ((x " ) * (x * ( pow (x,( - j))))) by Th15

          .= (((x " ) * x) * ( pow (x,( - j)))) by GROUP_1:def 3

          .= (( 1. L) * ( pow (x,( - j)))) by A1, VECTSP_1:def 10

          .= ( pow (x, 0 )) by A15

          .= ( 1. L) by Th13;

        end;

      end;

      

       A16: ( pow (x,( - j))) <> ( 0. L)

      proof

        per cases ;

          suppose 0 <= ( - j);

          then

          reconsider k = ( - j) as Element of NAT by INT_1: 3;

          ( pow (x,( - j))) = (x |^ k) by Def2;

          hence thesis by A1, Th1;

        end;

          suppose

           A17: ( - j) < 0 ;

          

           A18: (x |^ |.( - j).|) <> ( 0. L) by A1, Th1;

          ( pow (x,( - j))) = ((x |^ |.( - j).|) " ) by A17, Def2;

          hence thesis by A18, VECTSP_1: 25;

        end;

      end;

      

       A19: ( pow (x,(j - 1))) <> ( 0. L)

      proof

        per cases ;

          suppose 0 <= (j - 1);

          then

          reconsider k = (j - 1) as Element of NAT by INT_1: 3;

          ( pow (x,(j - 1))) = (x |^ k) by Def2;

          hence thesis by A1, Th1;

        end;

          suppose

           A20: (j - 1) < 0 ;

          

           A21: (x |^ |.(j - 1).|) <> ( 0. L) by A1, Th1;

          ( pow (x,(j - 1))) = ((x |^ |.(j - 1).|) " ) by A20, Def2;

          hence thesis by A21, VECTSP_1: 25;

        end;

      end;

      (( pow (x,(j - 1))) * ( pow (x,(1 - j)))) = (( pow (x,(j - 1))) * ( pow (x,( - (j - 1)))))

      .= (( pow (x,(j - 1))) * (( pow (x,(j - 1))) " )) by A1, Th18

      .= ( 1. L) by A2, VECTSP_1:def 10;

      then (x * ( pow (x,( - j)))) = ( pow (x,(1 - j))) by A5, A19, VECTSP_1: 5;

      

      then (( pow (x,(1 - j))) " ) = ((( pow (x,( - j))) " ) * (x " )) by A1, A16, Th2

      .= (( pow (x,( - ( - j)))) * (x " )) by A1, Th18

      .= (( pow (x,j)) * ( pow (x,( - 1)))) by Th15;

      then (( pow (x,j)) * ( pow (x,( - 1)))) = ( pow (x,( - (1 - j)))) by A1, Th18;

      hence thesis;

    end;

    theorem :: POLYNOM8:21

    

     Th21: for L be Field, i,j be Integer, x be Element of L st x <> ( 0. L) holds (( pow (x,i)) * ( pow (x,j))) = ( pow (x,(i + j)))

    proof

      let L be Field;

      let i,j be Integer;

      let x be Element of L;

      defpred P[ Integer] means for i be Integer holds ( pow (x,(i + $1))) = (( pow (x,i)) * ( pow (x,$1)));

      assume

       A1: x <> ( 0. L);

      

       A2: for j be Integer holds P[j] implies P[(j - 1)] & P[(j + 1)]

      proof

        let j be Integer;

        assume

         A3: for i be Integer holds ( pow (x,(i + j))) = (( pow (x,i)) * ( pow (x,j)));

        thus for i be Integer holds ( pow (x,(i + (j - 1)))) = (( pow (x,i)) * ( pow (x,(j - 1))))

        proof

          let i be Integer;

          

          thus ( pow (x,(i + (j - 1)))) = ( pow (x,((i - 1) + j)))

          .= (( pow (x,(i - 1))) * ( pow (x,j))) by A3

          .= ((( pow (x,i)) * ( pow (x,( - 1)))) * ( pow (x,j))) by A1, Th20

          .= (( pow (x,i)) * (( pow (x,( - 1))) * ( pow (x,j)))) by GROUP_1:def 3

          .= (( pow (x,i)) * ( pow (x,(j + ( - 1))))) by A3

          .= (( pow (x,i)) * ( pow (x,(j - 1))));

        end;

        let i be Integer;

        

        thus ( pow (x,(i + (j + 1)))) = ( pow (x,((i + 1) + j)))

        .= (( pow (x,(i + 1))) * ( pow (x,j))) by A3

        .= ((( pow (x,i)) * ( pow (x,1))) * ( pow (x,j))) by A1, Th19

        .= (( pow (x,i)) * (( pow (x,1)) * ( pow (x,j)))) by GROUP_1:def 3

        .= (( pow (x,i)) * ( pow (x,(j + 1)))) by A3;

      end;

      

       A4: P[ 0 ]

      proof

        let i be Integer;

        

        thus ( pow (x,(i + 0 ))) = (( pow (x,i)) * ( 1. L))

        .= (( pow (x,i)) * ( pow (x, 0 ))) by Th13;

      end;

      for j be Integer holds P[j] from INT_1:sch 4( A4, A2);

      hence thesis;

    end;

    

     Lm8: for L be almost_left_invertible associative well-unital add-associative right_zeroed right_complementable left-distributive commutative non degenerated non empty doubleLoopStr, k be Element of NAT , x be Element of L st x <> ( 0. L) holds ((x " ) |^ k) = ((x |^ k) " )

    proof

      let L be almost_left_invertible associative well-unital add-associative right_zeroed right_complementable left-distributive commutative non degenerated non empty doubleLoopStr;

      let k be Element of NAT ;

      let x be Element of L;

      

       A1: ( 1. L) <> ( 0. L);

      defpred P[ Nat] means ((x " ) |^ $1) = ((x |^ $1) " );

      assume

       A2: x <> ( 0. L);

       A3:

      now

        let n be Nat;

        assume

         A4: P[n];

        

         A5: (x |^ n) <> ( 0. L) by A2, Th1;

        ((x " ) |^ (n + 1)) = (((x " ) |^ n) * (x " )) by GROUP_1:def 7

        .= ((x * (x |^ n)) " ) by A2, A4, A5, Th2

        .= (((x |^ 1) * (x |^ n)) " ) by BINOM: 8

        .= ((x |^ (n + 1)) " ) by BINOM: 10;

        hence P[(n + 1)];

      end;

      ((x " ) |^ 0 ) = ( 1_ L) by BINOM: 8

      .= (( 1. L) * (( 1. L) " )) by A1, VECTSP_1:def 10

      .= (( 1_ L) " )

      .= ((x |^ 0 ) " ) by BINOM: 8;

      then

       A6: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A6, A3);

      hence thesis;

    end;

    theorem :: POLYNOM8:22

    

     Th22: for L be almost_left_invertible associative well-unital add-associative right_zeroed right_complementable left-distributive commutative non degenerated non empty doubleLoopStr, k be Element of NAT , x be Element of L st x <> ( 0. L) holds ( pow ((x " ),k)) = ( pow (x,( - k)))

    proof

      let L be almost_left_invertible associative well-unital add-associative right_zeroed right_complementable left-distributive commutative non degenerated non empty doubleLoopStr;

      let k be Element of NAT ;

      let x be Element of L;

      assume

       A1: x <> ( 0. L);

      ( pow ((x " ),k)) = ((x " ) |^ k) by Def2

      .= ((x |^ k) " ) by A1, Lm8

      .= (( pow (x,k)) " ) by Def2

      .= ( pow (x,( - k))) by A1, Th18;

      hence thesis;

    end;

    theorem :: POLYNOM8:23

    

     Th23: for L be Field, x be Element of L st x <> ( 0. L) holds for i,j,k be Nat holds (( pow (x,((i - 1) * (k - 1)))) * ( pow (x,( - ((j - 1) * (k - 1)))))) = ( pow (x,((i - j) * (k - 1))))

    proof

      let L be Field;

      let x be Element of L;

      assume

       A1: x <> ( 0. L);

      let i,j,k be Nat;

      (( pow (x,((i - 1) * (k - 1)))) * ( pow (x,( - ((j - 1) * (k - 1)))))) = ( pow (x,(((i - 1) * (k - 1)) + ( - ((j - 1) * (k - 1)))))) by A1, Th21

      .= ( pow (x,((i - j) * (k - 1))));

      hence thesis;

    end;

    theorem :: POLYNOM8:24

    

     Th24: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L, n,m be Element of NAT holds ( pow (x,(n * m))) = ( pow (( pow (x,n)),m))

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr;

      let x be Element of L;

      let n,m be Element of NAT ;

      ( pow (x,(n * m))) = (x |^ (n * m)) by Def2

      .= ((x |^ n) |^ m) by BINOM: 11

      .= ( pow ((x |^ n),m)) by Def2

      .= ( pow (( pow (x,n)),m)) by Def2;

      hence thesis;

    end;

    

     Lm9: for L be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non degenerated non empty doubleLoopStr, x be Element of L st x <> ( 0. L) holds for n be Element of NAT holds ( pow ((x " ),n)) = (( pow (x,n)) " )

    proof

      let L be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non degenerated non empty doubleLoopStr;

      let x be Element of L;

      

       A1: ( 1. L) <> ( 0. L);

      defpred P[ Nat] means ( pow ((x " ),$1)) = (( pow (x,$1)) " );

      assume

       A2: x <> ( 0. L);

      now

        let n be Nat;

        assume

         A3: P[n];

        

         A4: (x |^ n) <> ( 0. L) by A2, Th1;

        

        thus ( pow ((x " ),(n + 1))) = ((x " ) |^ (n + 1)) by Def2

        .= (((x " ) |^ n) * (x " )) by GROUP_1:def 7

        .= (( pow ((x " ),n)) * (x " )) by Def2

        .= (((( power L) . (x,n)) " ) * (x " )) by A3, Def2

        .= ((x * (x |^ n)) " ) by A2, A4, Th2

        .= (((x |^ 1) * (x |^ n)) " ) by BINOM: 8

        .= ((x |^ (n + 1)) " ) by BINOM: 10

        .= (( pow (x,(n + 1))) " ) by Def2;

        hence P[(n + 1)];

      end;

      then

       A5: for n be Nat st P[n] holds P[(n + 1)];

      let n be Nat;

      ( pow ((x " ), 0 )) = ( 1. L) by Th13

      .= (( 1. L) * (( 1. L) " )) by A1, VECTSP_1:def 10

      .= (( 1. L) " )

      .= (( pow (x, 0 )) " ) by Th13;

      then

       A6: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A6, A5);

      hence thesis;

    end;

    theorem :: POLYNOM8:25

    

     Th25: for L be Field, x be Element of L st x <> ( 0. L) holds for i be Integer holds ( pow ((x " ),i)) = (( pow (x,i)) " )

    proof

      let L be Field;

      let x be Element of L;

      assume

       A1: x <> ( 0. L);

      let i be Integer;

      per cases ;

        suppose i >= 0 ;

        then

        reconsider n = i as Element of NAT by INT_1: 3;

        

        thus ( pow ((x " ),i)) = (( pow (x,n)) " ) by A1, Lm9

        .= (( pow (x,i)) " );

      end;

        suppose

         A2: i < 0 ;

        

         A3: ( pow (x, |.i.|)) = (x |^ |.i.|) by Def2;

        

        thus ( pow ((x " ),i)) = (( pow ((x " ), |.i.|)) " ) by A2, Lm3

        .= ( pow (((x " ) " ), |.i.|)) by A1, Lm9, VECTSP_1: 25

        .= ( pow (x, |.i.|)) by A1, VECTSP_1: 24

        .= ((( pow (x, |.i.|)) " ) " ) by A1, A3, Th1, VECTSP_1: 24

        .= (( pow (x,i)) " ) by A2, Lm3;

      end;

    end;

    theorem :: POLYNOM8:26

    

     Th26: for L be Field, x be Element of L st x <> ( 0. L) holds for i,j be Integer holds ( pow (x,(i * j))) = ( pow (( pow (x,i)),j))

    proof

      let L be Field, x be Element of L;

      assume

       A1: x <> ( 0. L);

      let i,j be Integer;

      per cases ;

        suppose i >= 0 & j >= 0 ;

        then

        reconsider m = i, n = j as Element of NAT by INT_1: 3;

        

        thus ( pow (x,(i * j))) = ( pow (( pow (x,m)),n)) by Th24

        .= ( pow (( pow (x,i)),j));

      end;

        suppose

         A2: i >= 0 & j < 0 ;

        then

        reconsider m = i, n = ( - j) as Element of NAT by INT_1: 3;

        

         A3: ( pow (x,i)) = (x |^ m) by Def2;

        then

         A4: ( pow (x,i)) <> ( 0. L) by A1, Th1;

        

         A5: ( pow (( pow (x,i)),j)) = ((( pow (x,i)) |^ |.j.|) " ) by A2, Def2;

        (i * j) = ( - (i * n));

        

        hence ( pow (x,(i * j))) = (( pow (x,(i * n))) " ) by A1, Th18

        .= ( pow ((x " ),(i * n))) by A1, Th25

        .= ( pow (( pow ((x " ),m)),n)) by Th24

        .= ( pow ((( pow (x,i)) " ),n)) by A1, Th25

        .= (( pow ((( pow (x,i)) " ),j)) " ) by A4, Th18, VECTSP_1: 25

        .= ((( pow (( pow (x,i)),j)) " ) " ) by A1, A3, Th1, Th25

        .= ( pow (( pow (x,i)),j)) by A4, A5, Th1, VECTSP_1: 24;

      end;

        suppose

         A6: i < 0 & j >= 0 ;

        then

        reconsider m = ( - i), n = j as Element of NAT by INT_1: 3;

        

         A7: ( pow (x,i)) = ((x |^ |.i.|) " ) by A6, Def2;

        (i * j) = ( - (m * j));

        

        hence ( pow (x,(i * j))) = (( pow (x,(m * j))) " ) by A1, Th18

        .= ( pow ((x " ),(m * j))) by A1, Th25

        .= ( pow (( pow ((x " ),m)),n)) by Th24

        .= ( pow ((( pow ((x " ),i)) " ),n)) by A1, Th18, VECTSP_1: 25

        .= ( pow (((( pow (x,i)) " ) " ),j)) by A1, Th25

        .= ( pow (( pow (x,i)),j)) by A1, A7, Th1, VECTSP_1: 24;

      end;

        suppose

         A8: j < 0 & i < 0 ;

        then

        reconsider m = ( - i), n = ( - j) as Element of NAT by INT_1: 3;

        

         A9: ( pow (x,( - i))) = (x |^ m) by Def2;

        (x " ) <> ( 0. L) by A1, VECTSP_1: 25;

        then

         A10: ((x " ) |^ |.i.|) <> ( 0. L) by Th1;

        

         A11: ( pow ((x " ),i)) = (((x " ) |^ |.i.|) " ) by A8, Def2;

        ((i * j) * (( - 1) * ( - 1))) = (m * n);

        

        hence ( pow (x,(i * j))) = ( pow (( pow (x,m)),n)) by Th24

        .= (( pow (( pow (x,( - i))),j)) " ) by A1, A9, Th1, Th18

        .= (( pow ((( pow (x,i)) " ),j)) " ) by A1, Th18

        .= (( pow (( pow ((x " ),i)),j)) " ) by A1, Th25

        .= ( pow ((( pow ((x " ),i)) " ),j)) by A11, A10, Th25, VECTSP_1: 25

        .= ( pow (( pow (((x " ) " ),i)),j)) by A1, Th25, VECTSP_1: 25

        .= ( pow (( pow (x,i)),j)) by A1, VECTSP_1: 24;

      end;

    end;

    theorem :: POLYNOM8:27

    

     Th27: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L, i,k be Element of NAT st 1 <= k holds ( pow (x,(i * (k - 1)))) = ( pow ((x |^ i),(k - 1)))

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr;

      let x be Element of L;

      let i,k be Element of NAT ;

      assume 1 <= k;

      then 0 < k;

      then

      reconsider m = (k - 1) as Element of NAT by NAT_1: 20;

      ( pow (x,(i * (k - 1)))) = (x |^ (i * m)) by Def2

      .= ((x |^ i) |^ m) by BINOM: 11

      .= ( pow ((x |^ i),m)) by Def2;

      hence thesis;

    end;

    

     Lm10: for L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L, m be Element of NAT holds (x <> ( 0. L) & (x |^ m) = ( 1. L)) implies ((x " ) |^ m) = ( 1. L)

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, x be Element of L, m be Element of NAT ;

      assume x <> ( 0. L) & (x |^ m) = ( 1. L);

      then (( 1. L) * ((x " ) |^ m)) = ( 1. L) by Lm7;

      hence thesis;

    end;

    

     Lm11: for L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, x be Element of L, i be Element of NAT holds (x <> ( 0. L) & ((x " ) |^ i) = ( 1. L)) implies (x |^ i) = ( 1. L)

    proof

      let L be associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, x be Element of L, i be Element of NAT ;

      assume that

       A1: x <> ( 0. L) and

       A2: ((x " ) |^ i) = ( 1. L);

      

       A3: ( 1_ L) = (x |^ 0 ) by BINOM: 8;

      (((x " ) |^ i) * ( 1. L)) = ( 1. L) by A2;

      then (((x " ) |^ i) * (x |^ 0 )) = (((x " ) |^ i) * (x |^ i)) by A1, A3, Lm7;

      hence thesis by A1, A2, A3, VECTSP_1: 5;

    end;

    begin

    definition

      let m be Nat, L be non empty ZeroStr, p be AlgSequence of L;

      :: POLYNOM8:def4

      func mConv (p,m) -> Matrix of m, 1, L means

      : Def3: for i be Nat st 1 <= i & i <= m holds (it * (i,1)) = (p . (i - 1));

      existence

      proof

        defpred P[ Nat, set, set] means $3 = (p . ($1 - 1));

        reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

        

         A1: for i,j be Nat st [i, j] in [:( Seg m9), ( Seg 1):] holds ex x be Element of L st P[i, j, x]

        proof

          let i,j be Nat;

          assume

           A2: [i, j] in [:( Seg m9), ( Seg 1):];

          take (p /. (i - 1));

          ( [i, j] `1 ) in ( Seg m) by A2, MCART_1: 10;

          then i in ( Seg m);

          then 1 <= i by FINSEQ_1: 1;

          then ( dom p) = NAT & (1 - 1) <= (i - 1) by FUNCT_2:def 1, XREAL_1: 9;

          hence thesis by INT_1: 3, PARTFUN1:def 6;

        end;

        consider M be Matrix of m9, 1, L such that

         A3: for i,j be Nat st [i, j] in ( Indices M) holds P[i, j, (M * (i,j))] from MATRIX_0:sch 2( A1);

        reconsider M as Matrix of m, 1, L;

        take M;

        now

          let i be Nat;

          assume 1 <= i & i <= m;

          then

           A4: i in ( Seg m) & ( Indices M) = [:( Seg m), ( Seg 1):] by MATRIX_0: 23;

          1 in ( Seg 1);

          then [i, 1] in ( Indices M) by A4, ZFMISC_1:def 2;

          hence (M * (i,1)) = (p . (i - 1)) by A3;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of m, 1, L;

        assume that

         A5: for i be Nat st 1 <= i & i <= m holds (M1 * (i,1)) = (p . (i - 1)) and

         A6: for i be Nat st 1 <= i & i <= m holds (M2 * (i,1)) = (p . (i - 1));

        per cases ;

          suppose

           A7: m = 0 ;

          then

           A8: for i,j be Nat st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j)) by MATRIX_0: 22;

          

           A9: ( width M1) = 0 by A7, MATRIX_0: 22

          .= ( width M2) by A7, MATRIX_0: 22;

          ( len M1) = 0 by A7, MATRIX_0: 22

          .= ( len M2) by A7, MATRIX_0: 22;

          hence thesis by A9, A8, MATRIX_0: 21;

        end;

          suppose

           A10: m > 0 ;

           A11:

          now

            let i,j be Nat;

            assume [i, j] in ( Indices M1);

            then

             A12: [i, j] in [:( Seg m), ( Seg 1):] by A10, MATRIX_0: 23;

            then ( [i, j] `2 ) in ( Seg 1) by MCART_1: 10;

            then j in ( Seg 1);

            then 1 <= j & j <= 1 by FINSEQ_1: 1;

            then

             A13: j = 1 by XXREAL_0: 1;

            ( [i, j] `1 ) in ( Seg m) by A12, MCART_1: 10;

            then i in ( Seg m);

            then

             A14: 1 <= i & i <= m by FINSEQ_1: 1;

            

            hence (M1 * (i,j)) = (p . (i - 1)) by A5, A13

            .= (M2 * (i,j)) by A6, A14, A13;

          end;

          

           A15: ( width M1) = 1 by A10, MATRIX_0: 23

          .= ( width M2) by A10, MATRIX_0: 23;

          ( len M1) = m by A10, MATRIX_0: 23

          .= ( len M2) by A10, MATRIX_0: 23;

          hence thesis by A15, A11, MATRIX_0: 21;

        end;

      end;

    end

    theorem :: POLYNOM8:28

    

     Th28: for m be Nat st m > 0 holds for L be non empty ZeroStr, p be AlgSequence of L holds ( len ( mConv (p,m))) = m & ( width ( mConv (p,m))) = 1 & for i be Nat st i < m holds (( mConv (p,m)) * ((i + 1),1)) = (p . i)

    proof

      let m be Nat;

      assume

       A1: m > 0 ;

      let L be non empty ZeroStr, p be AlgSequence of L;

      set q = ( mConv (p,m));

      thus ( len q) = m by A1, MATRIX_0: 23;

      thus ( width q) = 1 by A1, MATRIX_0: 23;

      now

        let i be Nat;

        assume i < m;

        then ( 0 + 1) <= (i + 1) & (i + 1) <= m by NAT_1: 13;

        then (q * ((i + 1),1)) = (p . ((i + 1) - 1)) by Def3;

        hence (q * ((i + 1),1)) = (p . i);

      end;

      hence thesis;

    end;

    theorem :: POLYNOM8:29

    

     Th29: for m be Nat st m > 0 holds for L be non empty ZeroStr, a be AlgSequence of L, M be Matrix of m, 1, L holds (for i be Nat st i < m holds (M * ((i + 1),1)) = (a . i)) implies ( mConv (a,m)) = M

    proof

      let m be Nat;

      assume

       A1: m > 0 ;

      let L be non empty ZeroStr;

      let a be AlgSequence of L;

      let M be Matrix of m, 1, L;

      

       A2: ( width ( mConv (a,m))) = 1 by A1, Th28

      .= ( width M) by A1, MATRIX_0: 23;

      assume

       A3: for i be Nat st i < m holds (M * ((i + 1),1)) = (a . i);

      

       A4: for i,j be Nat st [i, j] in ( Indices ( mConv (a,m))) holds (( mConv (a,m)) * (i,j)) = (M * (i,j))

      proof

        let i,j be Nat;

        assume

         A5: [i, j] in ( Indices ( mConv (a,m)));

        then

         A6: i in ( dom ( mConv (a,m))) by ZFMISC_1: 87;

        ( len ( mConv (a,m))) = m by A1, Th28;

        then

         A7: i in ( Seg m) by A6, FINSEQ_1:def 3;

        then 0 < i by FINSEQ_1: 1;

        then

        reconsider k = (i - 1) as Nat by NAT_1: 20;

        

         A8: j in ( Seg ( width ( mConv (a,m)))) by A5, ZFMISC_1: 87;

        then

         A9: 1 <= j by FINSEQ_1: 1;

        j in ( Seg 1) by A1, A8, Th28;

        then

         A10: j <= 1 by FINSEQ_1: 1;

        (k + 1) <= m by A7, FINSEQ_1: 1;

        then

         A11: k < m by NAT_1: 13;

        

        then (M * ((k + 1),1)) = (a . k) by A3

        .= (( mConv (a,m)) * ((k + 1),1)) by A11, Th28

        .= (( mConv (a,m)) * (i,j)) by A9, A10, XXREAL_0: 1;

        hence thesis by A9, A10, XXREAL_0: 1;

      end;

      ( len ( mConv (a,m))) = m by A1, Th28

      .= ( len M) by A1, MATRIX_0: 23;

      hence thesis by A2, A4, MATRIX_0: 21;

    end;

    definition

      let L be non empty ZeroStr, M be Matrix of L;

      :: POLYNOM8:def5

      func aConv (M) -> AlgSequence of L means

      : Def4: (for i be Nat st i < ( len M) holds (it . i) = (M * ((i + 1),1))) & for i be Nat st i >= ( len M) holds (it . i) = ( 0. L);

      existence

      proof

        defpred P[ object, object] means ex k be Element of NAT st k = $1 & ((k < ( len M) & $2 = (M * ((k + 1),1))) or (( len M) <= k & $2 = ( 0. L)));

        

         A1: for x be object st x in NAT holds ex y be object st y in the carrier of L & P[x, y]

        proof

          let u be object;

          assume u in NAT ;

          then

          reconsider u9 = u as Element of NAT ;

          thus ex y be object st y in the carrier of L & P[u, y]

          proof

            per cases ;

              suppose

               A2: u9 < ( len M);

              take (M * ((u9 + 1),1));

              thus thesis by A2;

            end;

              suppose

               A3: u9 >= ( len M);

              take ( 0. L);

              thus thesis by A3;

            end;

          end;

        end;

        consider f be sequence of the carrier of L such that

         A4: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        reconsider f as sequence of L;

        ex n be Nat st for i be Nat st i >= n holds (f . i) = ( 0. L)

        proof

          take ( len M);

          now

            let i be Nat;

            i in NAT by ORDINAL1:def 12;

            then

             A5: ex k be Element of NAT st k = i & (k < ( len M) & (f . i) = (M * ((k + 1),1)) or ( len M) <= k & (f . i) = ( 0. L)) by A4;

            assume i >= ( len M);

            hence (f . i) = ( 0. L) by A5;

          end;

          hence thesis;

        end;

        then

        reconsider q = f as AlgSequence of L by ALGSEQ_1:def 1;

         A6:

        now

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          then

           A7: ex k be Element of NAT st k = i & (k < ( len M) & (q . i) = (M * ((k + 1),1)) or ( len M) <= k & (q . i) = ( 0. L)) by A4;

          assume i >= ( len M);

          hence (q . i) = ( 0. L) by A7;

        end;

        take q;

        now

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          then

           A8: ex k be Element of NAT st k = i & (k < ( len M) & (q . i) = (M * ((k + 1),1)) or ( len M) <= k & (q . i) = ( 0. L)) by A4;

          assume i < ( len M);

          hence (q . i) = (M * ((i + 1),1)) by A8;

        end;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let z1,z2 be AlgSequence of L;

        assume that

         A9: for i be Nat st i < ( len M) holds (z1 . i) = (M * ((i + 1),1)) and

         A10: for i be Nat st i >= ( len M) holds (z1 . i) = ( 0. L);

        assume that

         A11: for i be Nat st i < ( len M) holds (z2 . i) = (M * ((i + 1),1)) and

         A12: for i be Nat st i >= ( len M) holds (z2 . i) = ( 0. L);

         A13:

        now

          let u be object;

          assume u in ( dom z1);

          then

          reconsider u9 = u as Element of NAT by FUNCT_2:def 1;

          per cases ;

            suppose

             A14: u9 < ( len M);

            

            hence (z1 . u) = (M * ((u9 + 1),1)) by A9

            .= (z2 . u) by A11, A14;

          end;

            suppose

             A15: ( len M) <= u9;

            

            hence (z1 . u) = ( 0. L) by A10

            .= (z2 . u) by A12, A15;

          end;

        end;

        ( dom z1) = NAT by FUNCT_2:def 1

        .= ( dom z2) by FUNCT_2:def 1;

        hence z1 = z2 by A13, FUNCT_1: 2;

      end;

    end

    begin

    definition

      let L be well-unital non empty doubleLoopStr, x be Element of L, n be Element of NAT ;

      :: POLYNOM8:def6

      pred x is_primitive_root_of_degree n means n <> 0 & (x |^ n) = ( 1. L) & for i be Element of NAT st 0 < i & i < n holds (x |^ i) <> ( 1. L);

    end

    theorem :: POLYNOM8:30

    

     Th30: for L be well-unital add-associative right_zeroed right_complementable right-distributive non degenerated non empty doubleLoopStr, n be Element of NAT holds not (( 0. L) is_primitive_root_of_degree n)

    proof

      let L be well-unital add-associative right_zeroed right_complementable right-distributive non degenerated non empty doubleLoopStr, n be Element of NAT ;

      defpred P[ Nat] means (( 0. L) |^ $1) = ( 0. L);

      

       A1: for j be Nat st 1 <= j holds P[j] implies P[(j + 1)]

      proof

        let j be Nat;

        assume 1 <= j;

        assume P[j];

        (( 0. L) |^ (j + 1)) = ((( 0. L) |^ j) * ( 0. L)) by GROUP_1:def 7

        .= ( 0. L);

        hence thesis;

      end;

      

       A2: P[1] by BINOM: 8;

      

       A3: for m be Nat st 1 <= m holds P[m] from NAT_1:sch 8( A2, A1);

      assume

       A4: ( 0. L) is_primitive_root_of_degree n;

      then n <> 0 ;

      then ( 0 + 1) < (n + 1) by XREAL_1: 8;

      then 1 <= n by NAT_1: 13;

      then (( 0. L) |^ n) <> ( 1. L) by A3;

      hence contradiction by A4;

    end;

    theorem :: POLYNOM8:31

    

     Th31: for L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, m be Element of NAT , x be Element of L st x is_primitive_root_of_degree m holds (x " ) is_primitive_root_of_degree m

    proof

      let L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr;

      let m be Element of NAT ;

      let x be Element of L;

      assume

       A1: x is_primitive_root_of_degree m;

      then

       A2: x <> ( 0. L) by Th30;

      

       A3: for i be Element of NAT st 0 < i & i < m holds ((x " ) |^ i) <> ( 1. L)

      proof

        let i be Element of NAT ;

        assume 0 < i & i < m;

        then (x |^ i) <> ( 1. L) by A1;

        hence thesis by A2, Lm11;

      end;

      (x |^ m) = ( 1. L) by A1;

      then

       A4: ((x " ) |^ m) = ( 1. L) by A2, Lm10;

      m <> 0 by A1;

      hence thesis by A4, A3;

    end;

    theorem :: POLYNOM8:32

    

     Th32: for L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, m be Element of NAT , x be Element of L st x is_primitive_root_of_degree m holds for i,j be Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds ( pow (x,(i - j))) <> ( 1. L)

    proof

      let L be add-associative right_zeroed right_complementable associative commutative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr;

      let m be Element of NAT ;

      let x be Element of L;

      assume

       A1: x is_primitive_root_of_degree m;

      then

       A2: x <> ( 0. L) by Th30;

      let i,j be Nat;

      assume that

       A3: 1 <= i and

       A4: i <= m and

       A5: 1 <= j and

       A6: j <= m and

       A7: i <> j;

      per cases ;

        suppose

         A8: i > j;

        then

        reconsider k = (i - j) as Element of NAT by INT_1: 5;

        k <= (i - 1) by A5, XREAL_1: 13;

        then (k + 1) <= ((i - 1) + 1) by XREAL_1: 6;

        then k < i by NAT_1: 13;

        then

         A9: k < m by A4, XXREAL_0: 2;

        (i - j) > (j - j) by A8, XREAL_1: 14;

        then (x |^ k) <> ( 1. L) by A1, A9;

        hence thesis by Def2;

      end;

        suppose i <= j;

        then

         A10: i < j by A7, XXREAL_0: 1;

        then

         A11: (j - i) > (i - i) by XREAL_1: 14;

        

         A12: (i - j) < (j - j) by A10, XREAL_1: 14;

        then

         A13: |.(i - j).| = ( - (i - j)) by ABSVALUE:def 1;

        then

        reconsider k = ( - (i - j)) as Element of NAT ;

        (j - i) <= (j - 1) by A3, XREAL_1: 13;

        then (k + 1) <= ((j - 1) + 1) by XREAL_1: 6;

        then k < j by NAT_1: 13;

        then

         A14: k < m by A6, XXREAL_0: 2;

        

         A15: (x |^ k) <> ( 0. L) by A2, Th1;

        now

          assume ((x |^ k) " ) = ( 1. L);

          

          then ( 1. L) = ((x |^ k) * ( 1. L)) by A15, VECTSP_1:def 10

          .= (x |^ k);

          hence contradiction by A1, A11, A14;

        end;

        hence thesis by A12, A13, Def2;

      end;

    end;

    definition

      let m be Nat, L be well-unital non empty doubleLoopStr, p be Polynomial of L, x be Element of L;

      :: POLYNOM8:def7

      func DFT (p,x,m) -> AlgSequence of L means

      : Def6: (for i be Nat st i < m holds (it . i) = ( eval (p,(x |^ i)))) & for i be Nat st i >= m holds (it . i) = ( 0. L);

      existence

      proof

        defpred P[ object, object] means ex k be Element of NAT st k = $1 & ((k < m & $2 = ( eval (p,(x |^ k)))) or (m <= k & $2 = ( 0. L)));

        

         A1: for x be object st x in NAT holds ex y be object st y in the carrier of L & P[x, y]

        proof

          let u be object;

          assume u in NAT ;

          then

          reconsider u9 = u as Element of NAT ;

          per cases ;

            suppose

             A2: u9 < m;

            take ( eval (p,(x |^ u9)));

            thus thesis by A2;

          end;

            suppose

             A3: u9 >= m;

            take ( 0. L);

            thus thesis by A3;

          end;

        end;

        consider f be sequence of the carrier of L such that

         A4: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        reconsider f as sequence of L;

        ex n be Nat st for i be Nat st i >= n holds (f . i) = ( 0. L)

        proof

          reconsider m as Element of NAT by ORDINAL1:def 12;

          take m;

          now

            let i be Nat;

            i in NAT by ORDINAL1:def 12;

            then

             A5: ex k be Element of NAT st k = i & (k < m & (f . i) = ( eval (p,(x |^ k))) or m <= k & (f . i) = ( 0. L)) by A4;

            assume i >= m;

            hence (f . i) = ( 0. L) by A5;

          end;

          hence thesis;

        end;

        then

        reconsider q = f as AlgSequence of L by ALGSEQ_1:def 1;

         A6:

        now

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          then

           A7: ex k be Element of NAT st k = i & (k < m & (q . i) = ( eval (p,(x |^ k))) or m <= k & (q . i) = ( 0. L)) by A4;

          assume i >= m;

          hence (q . i) = ( 0. L) by A7;

        end;

        take q;

        now

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          then

           A8: ex k be Element of NAT st k = i & (k < m & (q . i) = ( eval (p,(x |^ k))) or m <= k & (q . i) = ( 0. L)) by A4;

          assume i < m;

          hence (q . i) = ( eval (p,(x |^ i))) by A8;

        end;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let z1,z2 be AlgSequence of L;

        assume that

         A9: for i be Nat st i < m holds (z1 . i) = ( eval (p,(x |^ i))) and

         A10: for i be Nat st i >= m holds (z1 . i) = ( 0. L);

        assume that

         A11: for i be Nat st i < m holds (z2 . i) = ( eval (p,(x |^ i))) and

         A12: for i be Nat st i >= m holds (z2 . i) = ( 0. L);

         A13:

        now

          let u be object;

          assume u in ( dom z1);

          then

          reconsider u9 = u as Element of NAT by FUNCT_2:def 1;

          per cases ;

            suppose

             A14: u9 < m;

            

            hence (z1 . u) = ( eval (p,(x |^ u9))) by A9

            .= (z2 . u) by A11, A14;

          end;

            suppose

             A15: m <= u9;

            

            hence (z1 . u) = ( 0. L) by A10

            .= (z2 . u) by A12, A15;

          end;

        end;

        ( dom z1) = NAT by FUNCT_2:def 1

        .= ( dom z2) by FUNCT_2:def 1;

        hence z1 = z2 by A13, FUNCT_1: 2;

      end;

    end

    theorem :: POLYNOM8:33

    

     Th33: for m be Nat, L be well-unital non empty doubleLoopStr, x be Element of L holds ( DFT (( 0_. L),x,m)) = ( 0_. L)

    proof

      let m be Nat, L be well-unital non empty doubleLoopStr, x be Element of L;

      set q = ( DFT (( 0_. L),x,m));

       A1:

      now

        let u be object;

        assume u in ( dom q);

        then

        reconsider n = u as Element of NAT by FUNCT_2:def 1;

        per cases ;

          suppose n < m;

          

          hence (q . u) = ( eval (( 0_. L),(x |^ n))) by Def6

          .= ( 0. L) by POLYNOM4: 17

          .= (( 0_. L) . n) by FUNCOP_1: 7

          .= (( 0_. L) . u);

        end;

          suppose n >= m;

          

          hence (q . u) = ( 0. L) by Def6

          .= (( 0_. L) . n) by FUNCOP_1: 7

          .= (( 0_. L) . u);

        end;

      end;

      ( dom q) = NAT by FUNCT_2:def 1

      .= ( dom ( 0_. L)) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: POLYNOM8:34

    

     Th34: for m be Nat, L be Field, p,q be Polynomial of L, x be Element of L holds (( DFT (p,x,m)) * ( DFT (q,x,m))) = ( DFT ((p *' q),x,m))

    proof

      let m be Nat;

      let L be Field;

      let p,q be Polynomial of L;

      let x be Element of L;

      set ep = ( DFT (p,x,m)), eq = ( DFT (q,x,m)), epq = ( DFT ((p *' q),x,m));

       A1:

      now

        let u9 be object;

        assume u9 in ( dom (ep * eq));

        then

        reconsider u = u9 as Element of NAT by FUNCT_2:def 1;

        per cases ;

          suppose

           A2: u < m;

          

          hence (epq . u9) = ( eval ((p *' q),(x |^ u))) by Def6

          .= (( eval (p,(x |^ u))) * ( eval (q,(x |^ u)))) by POLYNOM4: 24

          .= ((ep . u) * ( eval (q,(x |^ u)))) by A2, Def6

          .= ((ep . u) * (eq . u)) by A2, Def6

          .= ((ep * eq) . u9) by LOPBAN_3:def 7;

        end;

          suppose

           A3: m <= u;

          

          thus ((ep * eq) . u9) = ((ep . u) * (eq . u)) by LOPBAN_3:def 7

          .= (( 0. L) * (eq . u)) by A3, Def6

          .= ( 0. L)

          .= (epq . u9) by A3, Def6;

        end;

      end;

      ( dom (ep * eq)) = NAT by FUNCT_2:def 1

      .= ( dom epq) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    definition

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, m be Nat, x be Element of L;

      :: POLYNOM8:def8

      func Vandermonde (x,m) -> Matrix of m, L means

      : Def7: for i,j be Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (it * (i,j)) = ( pow (x,((i - 1) * (j - 1))));

      existence

      proof

        defpred P[ Nat, Nat, set] means $3 = ( pow (x,(($1 - 1) * ($2 - 1))));

        reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

        

         A1: for i,j be Nat st [i, j] in [:( Seg m9), ( Seg m9):] holds ex x be Element of L st P[i, j, x];

        consider M be Matrix of m9, m9, L such that

         A2: for i,j be Nat st [i, j] in ( Indices M) holds P[i, j, (M * (i,j))] from MATRIX_0:sch 2( A1);

        reconsider M as Matrix of m, m, L;

        take M;

        now

          let i be Nat;

          assume 1 <= i & i <= m;

          then

           A3: ( Indices M) = [:( Seg m), ( Seg m):] & i in ( Seg m) by MATRIX_0: 24;

          let j be Nat;

          assume 1 <= j & j <= m;

          then j in ( Seg m);

          then [i, j] in ( Indices M) by A3, ZFMISC_1:def 2;

          hence (M * (i,j)) = ( pow (x,((i - 1) * (j - 1)))) by A2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of m, L;

        assume

         A4: for i,j be Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (M1 * (i,j)) = ( pow (x,((i - 1) * (j - 1))));

        assume

         A5: for i,j be Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (M2 * (i,j)) = ( pow (x,((i - 1) * (j - 1))));

        now

          let i,j be Nat;

          

           A6: ( Indices M1) = [:( Seg m), ( Seg m):] by MATRIX_0: 24;

          assume [i, j] in ( Indices M1);

          then ex x,y be object st x in ( Seg m) & y in ( Seg m) & [x, y] = [i, j] by A6, ZFMISC_1:def 2;

          then

          consider z,y be set such that

           A7: [i, j] = [z, y] and

           A8: z in ( Seg m) and

           A9: y in ( Seg m);

          j = y by A7, XTUPLE_0: 1;

          then

           A10: 1 <= j & j <= m by A9, FINSEQ_1: 1;

          i = z by A7, XTUPLE_0: 1;

          then

           A11: 1 <= i & i <= m by A8, FINSEQ_1: 1;

          

          hence (M1 * (i,j)) = ( pow (x,((i - 1) * (j - 1)))) by A4, A10

          .= (M2 * (i,j)) by A5, A11, A10;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    notation

      let L be associative commutative well-unital distributive almost_left_invertible non empty doubleLoopStr, m be Nat, x be Element of L;

      synonym VM (x,m) for Vandermonde (x,m);

    end

    theorem :: POLYNOM8:35

    

     Th35: for L be Field, m,n be Nat st m > 0 holds for M be Matrix of m, n, L holds (( 1. (L,m)) * M) = M

    proof

      let L be Field, m,n be Nat;

      assume

       A1: m > 0 ;

      let M be Matrix of m, n, L;

      

       A2: ( width ( 1. (L,m))) = m by A1, MATRIX_0: 23

      .= ( len M) by A1, MATRIX_0: 23;

      set M2 = (( 1. (L,m)) * M);

      

       A3: ( len M) = m by A1, MATRIX_0: 23;

      ( len ( 1. (L,m))) = m by A1, MATRIX_0: 23;

      then

       A4: m = ( len M2) by A2, MATRIX_3:def 4;

       A5:

      now

        let i,j be Nat;

        assume

         A6: [i, j] in ( Indices M);

        then

         A7: i in ( dom M) by ZFMISC_1: 87;

        ( dom M) = ( Seg ( len M)) by FINSEQ_1:def 3

        .= ( dom M2) by A3, A4, FINSEQ_1:def 3;

        then ( Indices M) = ( Indices M2) by A2, MATRIX_3:def 4;

        

        then

         A8: (M2 * (i,j)) = (( Line (( 1. (L,m)),i)) "*" ( Col (M,j))) by A2, A6, MATRIX_3:def 4

        .= ( Sum ( mlt (( Line (( 1. (L,m)),i)),( Col (M,j))))) by FVSUM_1:def 9;

        ( len ( Line (( 1. (L,m)),i))) = ( width ( 1. (L,m))) by MATRIX_0:def 7

        .= m by MATRIX_0: 24;

        then

         A9: ( dom ( Line (( 1. (L,m)),i))) = ( Seg m) by FINSEQ_1:def 3;

        

         A10: ( len M) = m by A1, MATRIX_0: 23;

        then

         A11: i in ( dom ( Line (( 1. (L,m)),i))) by A7, A9, FINSEQ_1:def 3;

        

         A12: ( Indices ( 1. (L,m))) = [:( Seg m), ( Seg m):] by A1, MATRIX_0: 23;

        then

         A13: [i, i] in ( Indices ( 1. (L,m))) by A9, A11, ZFMISC_1: 87;

        

         A14: for k be Nat st k in ( dom ( Line (( 1. (L,m)),i))) & k <> i holds (( Line (( 1. (L,m)),i)) . k) = ( 0. L)

        proof

          let k be Nat;

          assume that

           A15: k in ( dom ( Line (( 1. (L,m)),i))) and

           A16: k <> i;

          

           A17: [i, k] in ( Indices ( 1. (L,m))) by A9, A11, A12, A15, ZFMISC_1: 87;

          k in ( Seg ( width ( 1. (L,m)))) by A9, A15, MATRIX_0: 24;

          

          then (( Line (( 1. (L,m)),i)) . k) = (( 1. (L,m)) * (i,k)) by MATRIX_0:def 7

          .= ( 0. L) by A16, A17, MATRIX_1:def 3;

          hence thesis;

        end;

        ( len ( Col (M,j))) = ( len M) by MATRIX_0:def 8

        .= m by A1, MATRIX_0: 23;

        then ( dom ( Col (M,j))) = ( Seg m) by FINSEQ_1:def 3;

        then

         A18: i in ( dom ( Col (M,j))) by A7, A10, FINSEQ_1:def 3;

        i in ( Seg ( width ( 1. (L,m)))) by A9, A11, MATRIX_0: 24;

        

        then

         A19: (( Line (( 1. (L,m)),i)) . i) = (( 1. (L,m)) * (i,i)) by MATRIX_0:def 7

        .= ( 1. L) by A13, MATRIX_1:def 3;

        i in ( dom ( Line (( 1. (L,m)),i))) by A7, A10, A9, FINSEQ_1:def 3;

        then ( Sum ( mlt (( Line (( 1. (L,m)),i)),( Col (M,j))))) = (( Col (M,j)) . i) by A19, A14, A18, MATRIX_3: 17;

        hence (M * (i,j)) = (M2 * (i,j)) by A8, A7, MATRIX_0:def 8;

      end;

      ( width M) = ( width M2) by A2, MATRIX_3:def 4;

      hence thesis by A3, A4, A5, MATRIX_0: 21;

    end;

    theorem :: POLYNOM8:36

    

     Th36: for L be Field, m be Element of NAT st 0 < m holds for u,v,u1 be Matrix of m, L holds (for i,j be Nat st 1 <= i & i <= m & 1 <= j & j <= m holds ((u * v) * (i,j)) = (( emb (m,L)) * (u1 * (i,j)))) implies (u * v) = (( emb (m,L)) * u1)

    proof

      let L be Field;

      let m be Element of NAT ;

      assume

       A1: m > 0 ;

      let u,v,u1 be Matrix of m, L;

      assume

       A2: for i,j be Nat st 1 <= i & i <= m & 1 <= j & j <= m holds ((u * v) * (i,j)) = (( emb (m,L)) * (u1 * (i,j)));

      

       A3: for i,j be Nat st [i, j] in ( Indices (u * v)) holds ((u * v) * (i,j)) = ((( emb (m,L)) * u1) * (i,j))

      proof

        let i,j be Nat;

        

         A4: [i, j] in ( Indices (u * v)) implies 1 <= i & i <= m & 1 <= j & j <= m

        proof

          ( width u) = m by MATRIX_0: 24

          .= ( len v) by MATRIX_0: 24;

          

          then

           A5: ( width (u * v)) = ( width v) by MATRIX_3:def 4

          .= m by MATRIX_0: 24;

          assume

           A6: [i, j] in ( Indices (u * v));

          then

           A7: j in ( Seg m) by A5, ZFMISC_1: 87;

          ( width u) = m by MATRIX_0: 24

          .= ( len v) by MATRIX_0: 24;

          

          then ( len (u * v)) = ( len u) by MATRIX_3:def 4

          .= m by MATRIX_0: 24;

          then (u * v) is Matrix of m, m, L by A1, A5, MATRIX_0: 20;

          then ( Indices (u * v)) = [:( Seg m), ( Seg m):] by A5, MATRIX_0: 25;

          then i in ( Seg m) by A6, ZFMISC_1: 87;

          hence thesis by A7, FINSEQ_1: 1;

        end;

        assume

         A8: [i, j] in ( Indices (u * v));

        then i in ( Seg m) & j in ( Seg m) by A4;

        then [i, j] in [:( Seg m), ( Seg m):] by ZFMISC_1: 87;

        then [i, j] in ( Indices u1) by MATRIX_0: 24;

        then ((( emb (m,L)) * u1) * (i,j)) = (( emb (m,L)) * (u1 * (i,j))) by MATRIX_3:def 5;

        hence thesis by A2, A8, A4;

      end;

      

       A9: ( width (( emb (m,L)) * u1)) = ( width u1) by MATRIX_3:def 5

      .= m by MATRIX_0: 24;

      ( width u) = m by MATRIX_0: 24

      .= ( len v) by MATRIX_0: 24;

      

      then

       A10: ( width (u * v)) = ( width v) by MATRIX_3:def 4

      .= m by MATRIX_0: 24;

      ( width u) = m by MATRIX_0: 24

      .= ( len v) by MATRIX_0: 24;

      

      then

       A11: ( len (u * v)) = ( len u) by MATRIX_3:def 4

      .= m by MATRIX_0: 24;

      ( len (( emb (m,L)) * u1)) = ( len u1) by MATRIX_3:def 5

      .= m by MATRIX_0: 24;

      hence thesis by A11, A9, A10, A3, MATRIX_0: 21;

    end;

    

     Lm12: for L be Field, m be Element of NAT st m > 0 holds for p,q be Polynomial of L holds (( emb ((2 * m),L)) * (( 1. (L,(2 * m))) * ( mConv ((p *' q),(2 * m))))) = (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m))))

    proof

      let L be Field, m be Element of NAT ;

      assume

       A1: m > 0 ;

      let p,q be Polynomial of L;

      (2 * m) > (2 * 0 ) by A1, XREAL_1: 68;

      hence thesis by Th35;

    end;

    theorem :: POLYNOM8:37

    

     Th37: for L be Field, x be Element of L, s be FinSequence of L, i,j,m be Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & ( len s) = m & for k be Nat st 1 <= k & k <= m holds (s /. k) = ( pow (x,((i - j) * (k - 1)))) holds ((( VM (x,m)) * ( VM ((x " ),m))) * (i,j)) = ( Sum s)

    proof

      let L be Field, x be Element of L, s be FinSequence of L, i,j,m be Element of NAT ;

      assume that

       A1: x is_primitive_root_of_degree m and

       A2: 1 <= i & i <= m and

       A3: 1 <= j and

       A4: j <= m and

       A5: ( len s) = m and

       A6: for k be Nat st 1 <= k & k <= m holds (s /. k) = ( pow (x,((i - j) * (k - 1))));

      ( len ( Line (( VM (x,m)),i))) = ( width ( VM (x,m))) by MATRIX_0:def 7

      .= m by MATRIX_0: 24

      .= ( len ( VM ((x " ),m))) by MATRIX_0: 24

      .= ( len ( Col (( VM ((x " ),m)),j))) by MATRIX_0:def 8;

      

      then

       A7: ( len ( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j))))) = ( len ( Line (( VM (x,m)),i))) by MATRIX_3: 6

      .= ( width ( VM (x,m))) by MATRIX_0:def 7

      .= m by MATRIX_0: 24;

      

       A8: x <> ( 0. L) by A1, Th30;

      

       A9: for k be Nat st 1 <= k & k <= m holds ((( Line (( VM (x,m)),i)) /. k) * (( Col (( VM ((x " ),m)),j)) /. k)) = ( pow (x,((i - j) * (k - 1))))

      proof

        ( len ( Col (( VM ((x " ),m)),j))) = ( len ( VM ((x " ),m))) by MATRIX_0:def 8

        .= m by MATRIX_0: 24;

        then

         A10: ( Seg m) = ( dom ( Col (( VM ((x " ),m)),j))) by FINSEQ_1:def 3;

        ( len ( Line (( VM (x,m)),i))) = ( width ( VM (x,m))) by MATRIX_0:def 7

        .= m by MATRIX_0: 24;

        then

         A11: ( Seg m) = ( dom ( Line (( VM (x,m)),i))) by FINSEQ_1:def 3;

        

         A12: (1 - 1) <= (j - 1) by A3, XREAL_1: 9;

        let k be Nat;

        assume that

         A13: 1 <= k and

         A14: k <= m;

        ( len ( VM ((x " ),m))) = m & k in ( Seg m) by A13, A14, MATRIX_0: 24;

        then

         A15: k in ( dom ( VM ((x " ),m))) by FINSEQ_1:def 3;

        k in ( Seg m) by A13, A14;

        then

         A16: (( Line (( VM (x,m)),i)) /. k) = (( Line (( VM (x,m)),i)) . k) by A11, PARTFUN1:def 6;

        (1 - 1) <= (k - 1) by A13, XREAL_1: 9;

        then

         A17: ((j - 1) * (k - 1)) in NAT by A12, INT_1: 3;

        ( width ( VM (x,m))) = m by MATRIX_0: 24;

        then k in ( Seg ( width ( VM (x,m)))) by A13, A14;

        then

         A18: (( Line (( VM (x,m)),i)) . k) = (( VM (x,m)) * (i,k)) by MATRIX_0:def 7;

        k in ( Seg m) by A13, A14;

        then

         A19: (( Col (( VM ((x " ),m)),j)) /. k) = (( Col (( VM ((x " ),m)),j)) . k) by A10, PARTFUN1:def 6;

        (( VM ((x " ),m)) * (k,j)) = ( pow ((x " ),((j - 1) * (k - 1)))) by A3, A4, A13, A14, Def7

        .= ( pow (x,( - ((j - 1) * (k - 1))))) by A8, A17, Th22;

        then (( Col (( VM ((x " ),m)),j)) . k) = ( pow (x,( - ((j - 1) * (k - 1))))) by A15, MATRIX_0:def 8;

        

        then ((( Line (( VM (x,m)),i)) /. k) * (( Col (( VM ((x " ),m)),j)) /. k)) = (( pow (x,((i - 1) * (k - 1)))) * ( pow (x,( - ((j - 1) * (k - 1)))))) by A2, A13, A14, A16, A18, A19, Def7

        .= ( pow (x,((i - j) * (k - 1)))) by A8, Th23;

        hence thesis;

      end;

      

       A20: for k be Nat st 1 <= k & k <= m holds (( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j)))) /. k) = (s /. k)

      proof

        ( len ( Col (( VM ((x " ),m)),j))) = ( len ( VM ((x " ),m))) by MATRIX_0:def 8

        .= m by MATRIX_0: 24;

        then

         A21: ( Seg m) = ( dom ( Col (( VM ((x " ),m)),j))) by FINSEQ_1:def 3;

        let k be Nat;

        ( len ( Line (( VM (x,m)),i))) = ( width ( VM (x,m))) by MATRIX_0:def 7

        .= m by MATRIX_0: 24;

        then

         A22: ( Seg m) = ( dom ( Line (( VM (x,m)),i))) by FINSEQ_1:def 3;

        assume

         A23: 1 <= k & k <= m;

        

        then

         A24: ((( Line (( VM (x,m)),i)) /. k) * (( Col (( VM ((x " ),m)),j)) /. k)) = ( pow (x,((i - j) * (k - 1)))) by A9

        .= (s /. k) by A6, A23;

        k in ( Seg m) by A23;

        then

         A25: (( Col (( VM ((x " ),m)),j)) . k) = (( Col (( VM ((x " ),m)),j)) /. k) by A21, PARTFUN1:def 6;

        ( Seg m) = ( dom ( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j))))) by A7, FINSEQ_1:def 3;

        then

         A26: k in ( dom ( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j))))) by A23;

        k in ( Seg m) by A23;

        then (( Line (( VM (x,m)),i)) . k) = (( Line (( VM (x,m)),i)) /. k) by A22, PARTFUN1:def 6;

        then (( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j)))) . k) = ((( Line (( VM (x,m)),i)) /. k) * (( Col (( VM ((x " ),m)),j)) /. k)) by A26, A25, FVSUM_1: 60;

        hence thesis by A26, A24, PARTFUN1:def 6;

      end;

      

       A27: for k be Nat st k in ( dom ( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j))))) holds (( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j)))) . k) = (s . k)

      proof

        let k be Nat;

        assume

         A28: k in ( dom ( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j)))));

        

         A29: ( Seg m) = ( dom ( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j))))) by A7, FINSEQ_1:def 3;

        then

         A30: 1 <= k & k <= m by A28, FINSEQ_1: 1;

        

         A31: k in ( dom s) by A5, A28, A29, FINSEQ_1:def 3;

        (( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j)))) . k) = (( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j)))) /. k) by A28, PARTFUN1:def 6

        .= (s /. k) by A20, A30

        .= (s . k) by A31, PARTFUN1:def 6;

        hence thesis;

      end;

      ( dom ( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j))))) = ( Seg m) by A7, FINSEQ_1:def 3

      .= ( dom s) by A5, FINSEQ_1:def 3;

      then

       A32: ( Sum ( mlt (( Line (( VM (x,m)),i)),( Col (( VM ((x " ),m)),j))))) = ( Sum s) by A27, FINSEQ_1: 13;

      ( width ( VM (x,m))) = m by MATRIX_0: 24;

      then

       A33: ( width ( VM (x,m))) = ( len ( VM ((x " ),m))) by MATRIX_0: 24;

      

       A34: ( width ( VM (x,m))) = m & ( len ( VM ((x " ),m))) = m by MATRIX_0: 24;

      ( len ( VM (x,m))) = m by MATRIX_0: 24;

      then

       A35: ( len (( VM (x,m)) * ( VM ((x " ),m)))) = m by A34, MATRIX_3:def 4;

      ( width ( VM ((x " ),m))) = m by MATRIX_0: 24;

      then ( width (( VM (x,m)) * ( VM ((x " ),m)))) = m by A34, MATRIX_3:def 4;

      then (( VM (x,m)) * ( VM ((x " ),m))) is Matrix of m, L by A2, A35, MATRIX_0: 20;

      then

       A36: ( Indices (( VM (x,m)) * ( VM ((x " ),m)))) = [:( Seg m), ( Seg m):] by MATRIX_0: 24;

      i in ( Seg m) & j in ( Seg m) by A2, A3, A4;

      then [i, j] in ( Indices (( VM (x,m)) * ( VM ((x " ),m)))) by A36, ZFMISC_1:def 2;

      then ((( VM (x,m)) * ( VM ((x " ),m))) * (i,j)) = (( Line (( VM (x,m)),i)) "*" ( Col (( VM ((x " ),m)),j))) by A33, MATRIX_3:def 4;

      hence thesis by A32, FVSUM_1:def 9;

    end;

    theorem :: POLYNOM8:38

    

     Th38: for L be Field, m,i,j be Element of NAT , x be Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds ((( VM (x,m)) * ( VM ((x " ),m))) * (i,j)) = ( 0. L)

    proof

      let L be Field, m,i,j be Element of NAT , x be Element of L;

      assume that

       A1: i <> j and

       A2: 1 <= i & i <= m & 1 <= j & j <= m and

       A3: x is_primitive_root_of_degree m;

      

       A4: x <> ( 0. L) by A3, Th30;

      

      then

       A5: ( pow (x,(m * (i - j)))) = ( pow (( pow (x,m)),(i - j))) by Th26

      .= ( pow ((x |^ m),(i - j))) by Def2

      .= ( pow (( 1. L),(i - j))) by A3

      .= ( 1. L) by Th16;

      ex G be FinSequence of L st (( dom G) = ( Seg m) & for k be Nat st k in ( Seg m) holds (G . k) = ( pow (x,((i - j) * (k - 1)))))

      proof

        defpred P[ Nat, set] means $2 = ( pow (x,((i - j) * ($1 - 1))));

        

         A6: for n be Nat st n in ( Seg m) holds ex x be Element of L st P[n, x];

        ex G be FinSequence of L st ( dom G) = ( Seg m) & for nn be Nat st nn in ( Seg m) holds P[nn, (G . nn)] from FINSEQ_1:sch 5( A6);

        hence thesis;

      end;

      then

      consider s be FinSequence of L such that

       A7: ( dom s) = ( Seg m) and

       A8: for k be Nat st k in ( Seg m) holds (s . k) = ( pow (x,((i - j) * (k - 1))));

      

       A9: for k be Nat st 1 <= k & k <= m holds (s /. k) = ( pow (x,((i - j) * (k - 1))))

      proof

        let k be Nat;

        assume

         A10: 1 <= k & k <= m;

        then

         A11: k in ( dom s) by A7;

        k in ( Seg m) by A10;

        

        then ( pow (x,((i - j) * (k - 1)))) = (s . k) by A8

        .= (s /. k) by A11, PARTFUN1:def 6;

        hence thesis;

      end;

      consider r be Element of L such that

       A12: r = ( pow (x,(i - j)));

      

       A13: ( len s) = m by A7, FINSEQ_1:def 3;

      for k be Nat st 1 <= k & k <= ( len s) holds (s . k) = (( pow (x,(i - j))) |^ (k -' 1))

      proof

        let k be Nat;

        assume that

         A14: 1 <= k and

         A15: k <= ( len s);

        

         A16: (1 - 1) <= (k - 1) by A14, XREAL_1: 9;

        (s . k) = (s /. k) by A14, A15, FINSEQ_4: 15

        .= ( pow (x,((i - j) * (k - 1)))) by A9, A13, A14, A15

        .= ( pow (x,((i - j) * (k -' 1)))) by A16, XREAL_0:def 2

        .= ( pow (( pow (x,(i - j))),(k -' 1))) by A4, Th26

        .= (( pow (x,(i - j))) |^ (k -' 1)) by Def2;

        hence thesis;

      end;

      

      then ( Sum s) = ((( 1. L) - (( pow (x,(i - j))) |^ ( len s))) / (( 1. L) - ( pow (x,(i - j))))) by A1, A2, A3, Th5, Th32

      .= ((( 1. L) - (( pow (x,(i - j))) |^ m)) / (( 1. L) - ( pow (x,(i - j))))) by A7, FINSEQ_1:def 3

      .= ((( 1. L) - ( pow (( pow (x,(i - j))),m))) / (( 1. L) - ( pow (x,(i - j))))) by Def2

      .= ((( 1. L) - ( pow (x,((i - j) * m)))) / (( 1. L) - ( pow (x,(i - j))))) by A4, Th26

      .= (( 0. L) / (( 1. L) - r)) by A5, A12, VECTSP_1: 19

      .= ( 0. L);

      hence thesis by A2, A3, A9, A13, Th37;

    end;

    theorem :: POLYNOM8:39

    

     Th39: for L be Field, m be Element of NAT st m > 0 holds for x be Element of L st x is_primitive_root_of_degree m holds (( VM (x,m)) * ( VM ((x " ),m))) = (( emb (m,L)) * ( 1. (L,m)))

    proof

      let L be Field, m be Element of NAT ;

      assume

       A1: m > 0 ;

      let x be Element of L;

      assume

       A2: x is_primitive_root_of_degree m;

      for i,j be Nat st i >= 1 & i <= m & j >= 1 & j <= m holds ((( VM (x,m)) * ( VM ((x " ),m))) * (i,j)) = (( emb (m,L)) * (( 1. (L,m)) * (i,j)))

      proof

        let i,j be Nat;

        

         A3: i in NAT & j in NAT by ORDINAL1:def 12;

        ex G be FinSequence of L st (( dom G) = ( Seg m) & for k be Nat st k in ( Seg m) holds (G . k) = ( pow (x,((i - j) * (k - 1)))))

        proof

          defpred P[ Nat, set] means $2 = ( pow (x,((i - j) * ($1 - 1))));

          

           A4: for n be Nat st n in ( Seg m) holds ex x be Element of L st P[n, x];

          ex G be FinSequence of L st ( dom G) = ( Seg m) & for nn be Nat st nn in ( Seg m) holds P[nn, (G . nn)] from FINSEQ_1:sch 5( A4);

          hence thesis;

        end;

        then

        consider s be FinSequence of L such that

         A5: ( dom s) = ( Seg m) and

         A6: for k be Nat st k in ( Seg m) holds (s . k) = ( pow (x,((i - j) * (k - 1))));

        

         A7: ( len s) = m by A5, FINSEQ_1:def 3;

        

         A8: for k be Nat st 1 <= k & k <= m holds (s /. k) = ( pow (x,((i - j) * (k - 1))))

        proof

          let k be Nat;

          assume

           A9: 1 <= k & k <= m;

          then

           A10: k in ( dom s) by A5;

          k in ( Seg m) by A9;

          

          then ( pow (x,((i - j) * (k - 1)))) = (s . k) by A6

          .= (s /. k) by A10, PARTFUN1:def 6;

          hence thesis;

        end;

        

         A11: ( Indices ( 1. (L,m))) = [:( Seg m), ( Seg m):] by MATRIX_0: 24;

        assume that

         A12: 1 <= i & i <= m and

         A13: 1 <= j & j <= m;

        per cases ;

          suppose

           A14: i = j;

          

           A15: for k be Element of NAT st 1 <= k & k <= m holds (s /. k) = ( 1. L)

          proof

            let k be Element of NAT ;

            assume 1 <= k & k <= m;

            

            then (s /. k) = ( pow (x,((i - j) * (k - 1)))) by A8

            .= ( 1. L) by A14, Th13;

            hence thesis;

          end;

          i in ( Seg m) by A12;

          then

           A16: [i, i] in ( Indices ( 1. (L,m))) by A11, ZFMISC_1: 87;

          ((( VM (x,m)) * ( VM ((x " ),m))) * (i,j)) = ( Sum s) by A2, A3, A12, A13, A7, A8, Th37

          .= (m * ( 1. L)) by A7, A15, Th4

          .= (( emb (m,L)) * ( 1. L));

          hence thesis by A14, A16, MATRIX_1:def 3;

        end;

          suppose

           A17: i <> j;

          i in ( Seg m) & j in ( Seg m) by A12, A13;

          then

           A18: [i, j] in ( Indices ( 1. (L,m))) by A11, ZFMISC_1: 87;

          ((( VM (x,m)) * ( VM ((x " ),m))) * (i,j)) = ( 0. L) by A2, A3, A12, A13, A17, Th38

          .= (( emb (m,L)) * ( 0. L));

          hence thesis by A17, A18, MATRIX_1:def 3;

        end;

      end;

      hence thesis by A1, Th36;

    end;

    theorem :: POLYNOM8:40

    

     Th40: for L be Field, m be Element of NAT , x be Element of L st m > 0 & x is_primitive_root_of_degree m holds (( VM (x,m)) * ( VM ((x " ),m))) = (( VM ((x " ),m)) * ( VM (x,m)))

    proof

      let L be Field;

      let m be Element of NAT ;

      let x be Element of L;

      assume that 0 < m and

       A1: x is_primitive_root_of_degree m;

      x <> ( 0. L) by A1, Th30;

      

      then (( VM ((x " ),m)) * ( VM (x,m))) = (( VM ((x " ),m)) * ( VM (((x " ) " ),m))) by VECTSP_1: 24

      .= (( emb (m,L)) * ( 1. (L,m))) by A1, Th31, Th39;

      hence thesis by A1, Th39;

    end;

    begin

    theorem :: POLYNOM8:41

    

     Th41: for L be Field, p be Polynomial of L, m be Element of NAT st m > 0 & ( len p) <= m holds for x be Element of L, i be Element of NAT st i < m holds (( DFT (p,x,m)) . i) = ((( VM (x,m)) * ( mConv (p,m))) * ((i + 1),1))

    proof

      let L be Field;

      let p be Polynomial of L;

      let m be Element of NAT ;

      assume that

       A1: m > 0 and

       A2: ( len p) <= m;

      let x be Element of L;

      set v = ( VM (x,m));

      for i be Element of NAT st i < m holds (( DFT (p,x,m)) . i) = ((v * ( mConv (p,m))) * ((i + 1),1))

      proof

        

         A3: for k be Nat st k < m holds (( Col (( mConv (p,m)),1)) . (k + 1)) = (p . k)

        proof

          let k be Nat;

          assume

           A4: k < m;

          then 1 <= (k + 1) & (k + 1) <= m by NAT_1: 11, NAT_1: 13;

          then

           A5: (k + 1) in ( Seg m);

          ( len ( mConv (p,m))) = m by A1, Th28;

          then (k + 1) in ( dom ( mConv (p,m))) by A5, FINSEQ_1:def 3;

          then (( Col (( mConv (p,m)),1)) . (k + 1)) = (( mConv (p,m)) * ((k + 1),1)) by MATRIX_0:def 8;

          hence thesis by A4, Th28;

        end;

        

         A6: ( width v) = m by MATRIX_0: 24

        .= ( len ( mConv (p,m))) by A1, Th28;

        

        then

         A7: ( len (v * ( mConv (p,m)))) = ( len v) by MATRIX_3:def 4

        .= m by MATRIX_0: 24;

        ( width (v * ( mConv (p,m)))) = ( width ( mConv (p,m))) by A6, MATRIX_3:def 4

        .= 1 by A1, Th28;

        then (v * ( mConv (p,m))) is Matrix of m, 1, L by A1, A7, MATRIX_0: 20;

        then

         A8: ( Indices (v * ( mConv (p,m)))) = [:( Seg m), ( Seg ( width (v * ( mConv (p,m))))):] by MATRIX_0: 25;

        

         A9: ( len ( mConv (p,m))) = m by A1, Th28

        .= ( width v) by MATRIX_0: 24;

        ( width (v * ( mConv (p,m)))) = ( width ( mConv (p,m))) by A6, MATRIX_3:def 4

        .= 1 by A1, Th28;

        then

         A10: 1 in ( Seg ( width (v * ( mConv (p,m)))));

        let i be Element of NAT ;

        assume

         A11: i < m;

        

         A12: for k be Nat st k < m holds (( Line (v,(i + 1))) . (k + 1)) = (v * ((i + 1),(k + 1)))

        proof

          let k be Nat;

          assume k < m;

          then 1 <= (k + 1) & (k + 1) <= m by NAT_1: 11, NAT_1: 13;

          then (k + 1) in ( Seg m);

          then (k + 1) in ( Seg ( width v)) by MATRIX_0: 24;

          hence thesis by MATRIX_0:def 7;

        end;

        

         A13: for k be Nat st k < m holds (( Line (v,(i + 1))) . (k + 1)) = ( pow (x,(i * k)))

        proof

          let k be Nat;

          assume

           A14: k < m;

          then

           A15: 1 <= (k + 1) & (k + 1) <= m by NAT_1: 11, NAT_1: 13;

          

           A16: 1 <= (i + 1) & (i + 1) <= m by A11, NAT_1: 11, NAT_1: 13;

          (( Line (v,(i + 1))) . (k + 1)) = (v * ((i + 1),(k + 1))) by A12, A14

          .= ( pow (x,(((i + 1) - 1) * ((k + 1) - 1)))) by A16, A15, Def7

          .= ( pow (x,(i * k)));

          hence thesis;

        end;

        

         A17: for k be Nat, a,b,c be Element of L st a = (( Line (v,(i + 1))) . (k + 1)) & b = (( Col (( mConv (p,m)),1)) . (k + 1)) & c = (p . k) holds k < m implies (a * b) = (( pow (x,(i * k))) * c)

        proof

          let k be Nat;

          let a,b,c be Element of L;

          assume that

           A18: a = (( Line (v,(i + 1))) . (k + 1)) and

           A19: b = (( Col (( mConv (p,m)),1)) . (k + 1)) & c = (p . k) and

           A20: k < m;

          a = ( pow (x,(i * k))) by A13, A18, A20;

          hence thesis by A3, A19, A20;

        end;

        

         A21: for k be Element of NAT st 1 <= k & k <= m holds (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k) = ((p . (k -' 1)) * (( power L) . ((x |^ i),(k -' 1))))

        proof

          

           A22: ( len ( mConv (p,m))) = m by A1, Th28;

          let k be Element of NAT ;

          assume that

           A23: 1 <= k and

           A24: k <= m;

          k in ( Seg m) by A23, A24;

          then k in ( dom ( mConv (p,m))) by A22, FINSEQ_1:def 3;

          then

           A25: (( Col (( mConv (p,m)),1)) . k) = (( mConv (p,m)) * (k,1)) by MATRIX_0:def 8;

           0 < k by A23;

          then ( dom p) = NAT & (k - 1) is Element of NAT by FUNCT_2:def 1, NAT_1: 20;

          then

           A26: (p . (k - 1)) = (p /. (k - 1)) by PARTFUN1:def 6;

          ( Seg ( width v)) = ( Seg m) by MATRIX_0: 24;

          then k in ( Seg ( width v)) by A23, A24;

          then (( Line (v,(i + 1))) . k) = (v * ((i + 1),k)) by MATRIX_0:def 7;

          then

          reconsider a = (( Line (v,(i + 1))) . k), b = (( Col (( mConv (p,m)),1)) . k), c = (p . (k - 1)) as Element of L by A25, A26;

          ( len ( Line (v,(i + 1)))) = ( width v) by MATRIX_0:def 7

          .= m by MATRIX_0: 24

          .= ( len ( mConv (p,m))) by A1, Th28

          .= ( len ( Col (( mConv (p,m)),1))) by MATRIX_0:def 8;

          

          then ( len ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) = ( len ( Line (v,(i + 1)))) by MATRIX_3: 6

          .= ( width v) by MATRIX_0:def 7

          .= m by MATRIX_0: 24;

          then ( dom ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) = ( Seg m) by FINSEQ_1:def 3;

          then k in ( dom ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) by A23, A24;

          then

           A27: (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k) = (a * b) by FVSUM_1: 60;

          

           A28: (a * b) = (( pow (x,(i * (k - 1)))) * c)

          proof

            

             A29: 0 < k by A23;

            then

             A30: (k - 1) is Nat by NAT_1: 20;

            (k - 1) <= (m - 1) & (m - 1) is Nat by A1, A24, NAT_1: 20, XREAL_1: 9;

            then

             A31: (k - 1) < ((m - 1) + 1) by A30, NAT_1: 13;

            reconsider l = (k - 1) as Nat by A29, NAT_1: 20;

            a = (( Line (v,(i + 1))) . (l + 1));

            hence thesis by A17, A31;

          end;

          reconsider d = ( pow (x,(i * (k - 1)))) as Element of L;

          

           A32: (k - 1) >= 0 by A23, NAT_1: 20;

          d = ( pow ((x |^ i),(k - 1))) by A23, Th27

          .= (( power L) . ((x |^ i),(k - 1))) by A32, Def2

          .= (( power L) . ((x |^ i),(k -' 1))) by A32, XREAL_0:def 2;

          hence thesis by A28, A27, A32, XREAL_0:def 2;

        end;

        

         A33: ( Sum ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) = ( eval (p,(x |^ i)))

        proof

          

           A34: for k be Nat st ( len p) < k & k <= m holds (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k) = ( 0. L)

          proof

            

             A35: 1 <= (1 + ( len p)) by NAT_1: 11;

            let k be Nat;

            assume that

             A36: ( len p) < k and

             A37: k <= m;

            

             A38: ( len p) < ((k - 1) + 1) by A36;

            (( len p) + 1) <= k by A36, NAT_1: 13;

            then

             A39: 1 <= k by A35, XXREAL_0: 2;

            then (1 - 1) <= (k - 1) by XREAL_1: 9;

            then (k -' 1) = (k - 1) by XREAL_0:def 2;

            then

             A40: (k -' 1) >= ( len p) by A38, NAT_1: 13;

            k in NAT by ORDINAL1:def 12;

            

            then (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k) = ((p . (k -' 1)) * (( power L) . ((x |^ i),(k -' 1)))) by A21, A37, A39

            .= (( 0. L) * (( power L) . ((x |^ i),(k -' 1)))) by A40, ALGSEQ_1: 8

            .= ( 0. L);

            hence thesis;

          end;

          ( len ( Line (v,(i + 1)))) = ( width v) by MATRIX_0:def 7

          .= m by MATRIX_0: 24

          .= ( len ( mConv (p,m))) by A1, Th28

          .= ( len ( Col (( mConv (p,m)),1))) by MATRIX_0:def 8;

          

          then

           A41: ( len ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) = ( len ( Line (v,(i + 1)))) by MATRIX_3: 6

          .= ( width v) by MATRIX_0:def 7

          .= m by MATRIX_0: 24;

          (( len p) - ( len p)) <= (m - ( len p)) by A2, XREAL_1: 9;

          then

          reconsider lengthG = (m - ( len p)) as Element of NAT by INT_1: 3;

          consider F be FinSequence of L such that

           A42: ( eval (p,(x |^ i))) = ( Sum F) and

           A43: ( len F) = ( len p) and

           A44: for k be Element of NAT st k in ( dom F) holds (F . k) = ((p . (k -' 1)) * (( power L) . ((x |^ i),(k -' 1)))) by POLYNOM4:def 2;

          ex G be FinSequence of L st (( dom G) = ( Seg lengthG) & for k be Nat st k in ( Seg lengthG) holds (G . k) = ( 0. L))

          proof

            defpred P[ set, set] means $2 = ( 0. L);

            

             A45: for n be Nat st n in ( Seg lengthG) holds ex x be Element of L st P[n, x];

            ex G be FinSequence of L st ( dom G) = ( Seg lengthG) & for nn be Nat st nn in ( Seg lengthG) holds P[nn, (G . nn)] from FINSEQ_1:sch 5( A45);

            hence thesis;

          end;

          then

          consider G be FinSequence of L such that

           A46: ( dom G) = ( Seg lengthG) and

           A47: for k be Nat st k in ( Seg lengthG) holds (G . k) = ( 0. L);

          

           A48: for k be Element of NAT st k in ( Seg lengthG) holds (G . k) = ( 0. L) by A47;

          

           A49: ( len G) = (m - ( len p)) by A46, FINSEQ_1:def 3;

          then (( len F) + ( len G)) = m by A43;

          then ( dom (F ^ G)) = ( Seg m) by FINSEQ_1:def 7;

          then

           A50: ( dom ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) = ( dom (F ^ G)) by A41, FINSEQ_1:def 3;

          

           A51: for k be Element of NAT st 1 <= k & k <= ( len p) holds (F . k) = (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k)

          proof

            let k be Element of NAT ;

            assume that

             A52: 1 <= k and

             A53: k <= ( len p);

            

             A54: k <= m by A2, A53, XXREAL_0: 2;

            ( dom F) = ( Seg ( len p)) by A43, FINSEQ_1:def 3;

            then k in ( dom F) by A52, A53;

            

            then (F . k) = ((p . (k -' 1)) * (( power L) . ((x |^ i),(k -' 1)))) by A44

            .= (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k) by A21, A52, A54;

            hence thesis;

          end;

          for k be Nat st k in ( dom ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) holds (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k) = ((F ^ G) . k)

          proof

            let k be Nat;

            (( len F) + ( len G)) = m by A43, A49;

            then

             A55: ( dom (F ^ G)) = ( Seg m) by FINSEQ_1:def 7;

            assume

             A56: k in ( dom ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))));

            per cases by A50, A56, A55, FINSEQ_1: 1;

              suppose

               A57: 1 <= k & k <= ( len F);

              then k in ( dom F) by FINSEQ_3: 25;

              

              then ((F ^ G) . k) = (F . k) by FINSEQ_1:def 7

              .= (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k) by A43, A51, A56, A57;

              hence thesis;

            end;

              suppose

               A58: ( len F) < k & k <= m;

              then (( len F) + 1) <= k by NAT_1: 13;

              then ((( len F) + 1) - ( len F)) <= (k - ( len F)) by XREAL_1: 9;

              then

              reconsider l = (k - ( len F)) as Element of NAT by INT_1: 3;

              (( len p) - m) <= (m - m) by A2, XREAL_1: 9;

              then ( - (( len p) - m)) >= 0 ;

              then

              reconsider lengthG = (m - ( len p)) as Element of NAT by INT_1: 3;

              (( len F) + 1) <= k by A58, NAT_1: 13;

              then

               A59: ((( len F) + 1) - ( len F)) <= (k - ( len F)) by XREAL_1: 9;

              l <= lengthG by A43, A58, XREAL_1: 9;

              then

               A60: l in ( dom G) by A46, A59;

              (( len F) + ( len G)) = m by A43, A49;

              then ( dom (F ^ G)) = ( Seg m) by FINSEQ_1:def 7;

              then ( len (F ^ G)) = m by FINSEQ_1:def 3;

              

              then ((F ^ G) . k) = (G . (k - ( len F))) by A58, FINSEQ_1: 24

              .= ( 0. L) by A46, A47, A60

              .= (( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) . k) by A43, A34, A58;

              hence thesis;

            end;

          end;

          then ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1)))) = (F ^ G) by A50, FINSEQ_1: 13;

          

          then ( Sum ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) = (( Sum F) + ( Sum G)) by RLVECT_1: 41

          .= (( Sum F) + ( 0. L)) by A46, A48, POLYNOM3: 1

          .= ( eval (p,(x |^ i))) by A42, RLVECT_1:def 4;

          hence thesis;

        end;

        

         A61: (( Line (v,(i + 1))) "*" ( Col (( mConv (p,m)),1))) = ( Sum ( mlt (( Line (v,(i + 1))),( Col (( mConv (p,m)),1))))) by FVSUM_1:def 9;

        1 <= (i + 1) & (i + 1) <= m by A11, NAT_1: 11, NAT_1: 13;

        then (i + 1) in ( Seg m);

        then [(i + 1), 1] in ( Indices (v * ( mConv (p,m)))) by A8, A10, ZFMISC_1:def 2;

        then ((v * ( mConv (p,m))) * ((i + 1),1)) = ( eval (p,(x |^ i))) by A9, A61, A33, MATRIX_3:def 4;

        hence thesis by A11, Def6;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM8:42

    

     Th42: for L be Field, p be Polynomial of L holds for m be Nat st 0 < m & ( len p) <= m holds for x be Element of L holds ( DFT (p,x,m)) = ( aConv (( VM (x,m)) * ( mConv (p,m))))

    proof

      let L be Field;

      let p be Polynomial of L;

      let m be Nat;

      assume that

       A1: 0 < m and

       A2: ( len p) <= m;

      let x be Element of L;

      

       A3: m in NAT by ORDINAL1:def 12;

       A4:

      now

        let u9 be object;

        assume u9 in ( dom ( DFT (p,x,m)));

        then

        reconsider u = u9 as Element of NAT by FUNCT_2:def 1;

        per cases ;

          suppose

           A5: u < m;

          ( width ( VM (x,m))) = m by MATRIX_0: 24

          .= ( len ( mConv (p,m))) by A1, Th28;

          

          then

           A6: ( len (( VM (x,m)) * ( mConv (p,m)))) = ( len ( VM (x,m))) by MATRIX_3:def 4

          .= m by MATRIX_0: 24;

          

          thus (( DFT (p,x,m)) . u9) = ((( VM (x,m)) * ( mConv (p,m))) * ((u + 1),1)) by A3, A2, A5, Th41

          .= (( aConv (( VM (x,m)) * ( mConv (p,m)))) . u9) by A5, A6, Def4;

        end;

          suppose

           A7: m <= u;

          ( width ( VM (x,m))) = m by MATRIX_0: 24

          .= ( len ( mConv (p,m))) by A1, Th28;

          

          then

           A8: ( len (( VM (x,m)) * ( mConv (p,m)))) = ( len ( VM (x,m))) by MATRIX_3:def 4

          .= m by MATRIX_0: 24;

          

          thus (( DFT (p,x,m)) . u9) = ( 0. L) by A7, Def6

          .= (( aConv (( VM (x,m)) * ( mConv (p,m)))) . u9) by A7, A8, Def4;

        end;

      end;

      ( dom ( DFT (p,x,m))) = NAT by FUNCT_2:def 1

      .= ( dom ( aConv (( VM (x,m)) * ( mConv (p,m))))) by FUNCT_2:def 1;

      hence thesis by A4, FUNCT_1: 2;

    end;

    theorem :: POLYNOM8:43

    

     Th43: for L be Field, p,q be Polynomial of L, m be Element of NAT st m > 0 & ( len p) <= m & ( len q) <= m holds for x be Element of L st x is_primitive_root_of_degree (2 * m) holds ( DFT (( DFT ((p *' q),x,(2 * m))),(x " ),(2 * m))) = (( emb ((2 * m),L)) * (p *' q))

    proof

      let L be Field;

      let p,q be Polynomial of L;

      let m be Element of NAT ;

      assume that

       A1: m > 0 and

       A2: ( len p) <= m & ( len q) <= m;

      let x be Element of L;

      assume

       A3: x is_primitive_root_of_degree (2 * m);

      per cases ;

        suppose

         A4: ( len p) = 0 or ( len q) = 0 ;

        per cases by A4;

          suppose ( len p) = 0 ;

          then p = ( 0_. L) by POLYNOM4: 5;

          then (p *' q) = ( 0_. L) by POLYNOM3: 34;

          then (( emb ((2 * m),L)) * (p *' q)) = ( 0_. L) & ( DFT (( DFT ((p *' q),x,(2 * m))),(x " ),(2 * m))) = ( DFT (( 0_. L),(x " ),(2 * m))) by Th33, POLYNOM5: 28;

          hence thesis by Th33;

        end;

          suppose ( len q) = 0 ;

          then q = ( 0_. L) by POLYNOM4: 5;

          then (p *' q) = ( 0_. L) by POLYNOM3: 34;

          then (( emb ((2 * m),L)) * (p *' q)) = ( 0_. L) & ( DFT (( DFT ((p *' q),x,(2 * m))),(x " ),(2 * m))) = ( DFT (( 0_. L),(x " ),(2 * m))) by Th33, POLYNOM5: 28;

          hence thesis by Th33;

        end;

      end;

        suppose

         A5: ( len p) <> 0 & ( len q) <> 0 ;

        set v1 = ( VM (x,(2 * m))), v2 = ( VM ((x " ),(2 * m)));

        

         A6: (( len p) + ( len q)) <= (m + m) by A2, XREAL_1: 7;

        ( len (p *' q)) <= (( len p) + ( len q)) by A5, Th9;

        then

         A7: ( len (p *' q)) <= (2 * m) by A6, XXREAL_0: 2;

        

         A8: for i be Nat st i < (2 * m) holds ((v1 * ( mConv ((p *' q),(2 * m)))) * ((i + 1),1)) = (( DFT ((p *' q),x,(2 * m))) . i)

        proof

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          hence thesis by A7, Th41;

        end;

        for i be Nat st i >= (2 * m) holds (( DFT ((p *' q),x,(2 * m))) . i) = ( 0. L) by Def6;

        then (2 * m) is_at_least_length_of ( DFT ((p *' q),x,(2 * m))) by ALGSEQ_1:def 2;

        then

         A9: ( len ( DFT ((p *' q),x,(2 * m)))) <= (2 * m) by ALGSEQ_1:def 3;

        

         A10: ( width v2) = (2 * m) by MATRIX_0: 24

        .= ( len v1) by MATRIX_0: 24;

        

         A11: (m + m) <> 0 by A1;

        

         A12: (v2 * v1) = (v1 * v2) by A3, Th40

        .= (( emb ((2 * m),L)) * ( 1. (L,(2 * m)))) by A3, Th39;

         A13:

        now

          let u9 be object;

          assume u9 in ( dom ( aConv (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m))))));

          then

          reconsider u = u9 as Element of NAT by FUNCT_2:def 1;

          per cases ;

            suppose

             A14: u < (2 * m);

            then ( 0 + 1) <= (u + 1) & (u + 1) <= (2 * m) by NAT_1: 13;

            then

             A15: (u + 1) in ( Seg (2 * m));

            ( len ( mConv ((p *' q),(2 * m)))) = (2 * m) by A11, Th28;

            then

             A16: ( dom ( mConv ((p *' q),(2 * m)))) = ( Seg (2 * m)) by FINSEQ_1:def 3;

            ( Seg ( width ( mConv ((p *' q),(2 * m))))) = ( Seg 1) & 1 in ( Seg 1) by A11, Th28;

            then

             A17: [(u + 1), 1] in ( Indices ( mConv ((p *' q),(2 * m)))) by A16, A15, ZFMISC_1: 87;

            ( len (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m))))) = ( len ( mConv ((p *' q),(2 * m)))) by MATRIX_3:def 5

            .= (2 * m) by A11, Th28;

            

            hence (( aConv (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m))))) . u9) = ((( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m)))) * ((u + 1),1)) by A14, Def4

            .= (( emb ((2 * m),L)) * (( mConv ((p *' q),(2 * m))) * ((u + 1),1))) by A17, MATRIX_3:def 5

            .= (( emb ((2 * m),L)) * ((p *' q) . u)) by A14, Th28

            .= ((( emb ((2 * m),L)) * (p *' q)) . u9) by POLYNOM5:def 4;

          end;

            suppose

             A18: (2 * m) <= u;

            ( len (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m))))) = ( len ( mConv ((p *' q),(2 * m)))) by MATRIX_3:def 5

            .= (2 * m) by A11, Th28;

            

            hence (( aConv (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m))))) . u9) = ( 0. L) by A18, Def4

            .= (( emb ((2 * m),L)) * ( 0. L))

            .= (( emb ((2 * m),L)) * ((p *' q) . u)) by A7, A18, ALGSEQ_1: 8, XXREAL_0: 2

            .= ((( emb ((2 * m),L)) * (p *' q)) . u9) by POLYNOM5:def 4;

          end;

        end;

        ( dom ( aConv (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m)))))) = NAT by FUNCT_2:def 1

        .= ( dom (( emb ((2 * m),L)) * (p *' q))) by FUNCT_2:def 1;

        then

         A19: ( aConv (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m))))) = (( emb ((2 * m),L)) * (p *' q)) by A13, FUNCT_1: 2;

        

         A20: ( len ( mConv ((p *' q),(2 * m)))) = (2 * m) by A11, Th28

        .= ( width v1) by MATRIX_0: 24;

        

        then

         A21: ( len (v1 * ( mConv ((p *' q),(2 * m))))) = ( len v1) by MATRIX_3:def 4

        .= (2 * m) by MATRIX_0: 24;

        ( width (v1 * ( mConv ((p *' q),(2 * m))))) = ( width ( mConv ((p *' q),(2 * m)))) by A20, MATRIX_3:def 4

        .= 1 by A11, Th28;

        then (v1 * ( mConv ((p *' q),(2 * m)))) is Matrix of (2 * m), 1, L by A11, A21, MATRIX_0: 20;

        

        then ( aConv (v2 * ( mConv (( DFT ((p *' q),x,(2 * m))),(2 * m))))) = ( aConv (v2 * (v1 * ( mConv ((p *' q),(2 * m)))))) by A11, A8, Th29

        .= ( aConv ((v2 * v1) * ( mConv ((p *' q),(2 * m))))) by A10, A20, MATRIX_3: 33

        .= ( aConv (( emb ((2 * m),L)) * (( 1. (L,(2 * m))) * ( mConv ((p *' q),(2 * m)))))) by A11, A12, Th6

        .= ( aConv (( emb ((2 * m),L)) * ( mConv ((p *' q),(2 * m))))) by A1, Lm12;

        hence thesis by A11, A9, A19, Th42;

      end;

    end;

    ::$Notion-Name

    theorem :: POLYNOM8:44

    for L be Field, p,q be Polynomial of L, m be Element of NAT st m > 0 & ( len p) <= m & ( len q) <= m holds for x be Element of L st x is_primitive_root_of_degree (2 * m) holds ( emb ((2 * m),L)) <> ( 0. L) implies ((( emb ((2 * m),L)) " ) * ( DFT ((( DFT (p,x,(2 * m))) * ( DFT (q,x,(2 * m)))),(x " ),(2 * m)))) = (p *' q)

    proof

      let L be Field;

      let p,q be Polynomial of L;

      let m be Element of NAT ;

      assume

       A1: m > 0 & ( len p) <= m & ( len q) <= m;

      let x be Element of L;

      assume

       A2: x is_primitive_root_of_degree (2 * m);

      assume

       A3: ( emb ((2 * m),L)) <> ( 0. L);

      ((( emb ((2 * m),L)) " ) * ( DFT ((( DFT (p,x,(2 * m))) * ( DFT (q,x,(2 * m)))),(x " ),(2 * m)))) = ((( emb ((2 * m),L)) " ) * ( DFT (( DFT ((p *' q),x,(2 * m))),(x " ),(2 * m)))) by Th34

      .= ((( emb ((2 * m),L)) " ) * (( emb ((2 * m),L)) * (p *' q))) by A1, A2, Th43

      .= (((( emb ((2 * m),L)) " ) * ( emb ((2 * m),L))) * (p *' q)) by Th10

      .= (( 1. L) * (p *' q)) by A3, VECTSP_1:def 10

      .= (p *' q) by POLYNOM5: 27;

      hence thesis;

    end;