algnum_1.miz



    begin

    reserve i,j for Nat;

    reserve A,B for Ring;

    theorem :: ALGNUM_1:1

    

     Th1: for L1,L2,L3 be Ring st L1 is Subring of L2 & L2 is Subring of L3 holds L1 is Subring of L3

    proof

      let L1,L2,L3 be Ring;

      assume that

       A1: L1 is Subring of L2 and

       A2: L2 is Subring of L3;

      

       A3: the carrier of L1 c= the carrier of L2 & the addF of L1 = (the addF of L2 || the carrier of L1) & the multF of L1 = (the multF of L2 || the carrier of L1) & ( 1. L1) = ( 1. L2) & ( 0. L1) = ( 0. L2) by A1, C0SP1:def 3;

      

       A4: the carrier of L2 c= the carrier of L3 & the addF of L2 = (the addF of L3 || the carrier of L2) & the multF of L2 = (the multF of L3 || the carrier of L2) & ( 1. L2) = ( 1. L3) & ( 0. L2) = ( 0. L3) by A2, C0SP1:def 3;

      set A1 = [:the carrier of L1, the carrier of L1:];

      set A2 = [:the carrier of L2, the carrier of L2:];

      set A3 = [:the carrier of L3, the carrier of L3:];

      

       A8: the carrier of L1 c= the carrier of L3 by A3, A4;

      

       A9: the addF of L1 = (the addF of L2 || the carrier of L1) by A1, C0SP1:def 3

      .= ((the addF of L3 || the carrier of L2) || the carrier of L1) by A2, C0SP1:def 3

      .= (the addF of L3 || the carrier of L1) by A3, ZFMISC_1: 96, RELAT_1: 74;

      

       A10: the multF of L1 = (the multF of L2 || the carrier of L1) by A1, C0SP1:def 3

      .= ((the multF of L3 || the carrier of L2) || the carrier of L1) by A2, C0SP1:def 3

      .= (the multF of L3 || the carrier of L1) by A3, ZFMISC_1: 96, RELAT_1: 74;

      

       A11: ( 1. L1) = ( 1. L2) by A1, C0SP1:def 3

      .= ( 1. L3) by A2, C0SP1:def 3;

      ( 0. L1) = ( 0. L2) by A1, C0SP1:def 3

      .= ( 0. L3) by A2, C0SP1:def 3;

      hence thesis by A8, A9, A10, A11, C0SP1:def 3;

    end;

    theorem :: ALGNUM_1:2

    

     Lm1: F_Rat is Subfield of F_Complex by EC_PF_1: 5, GAUSSINT: 14, RING_3: 48;

    theorem :: ALGNUM_1:3

    

     Th3: F_Rat is Subring of F_Complex by RING_3: 43, Lm1;

    theorem :: ALGNUM_1:4

    

     Th4: INT.Ring is Subring of F_Complex by RING_3: 47, Th3, Th1;

    

     Lm5: A is Subring of B implies ( In (( 0. A),B)) = ( 0. B) & ( In (( 1. A),B)) = ( 1. B)

    proof

      assume

       A1: A is Subring of B;

      

      then

       A2: ( In (( 0. A),B)) = ( In (( 0. B),B)) by C0SP1:def 3

      .= ( 0. B) by SUBSET_1:def 8;

      ( In (( 1. A),B)) = ( In (( 1. B),B)) by A1, C0SP1:def 3

      .= ( 1. B) by SUBSET_1:def 8;

      hence thesis by A2;

    end;

    

     Lm6: for a be Element of A st A is Subring of B holds a is Element of B

    proof

      let a be Element of A;

      assume A is Subring of B;

      then the carrier of A c= the carrier of B by C0SP1:def 3;

      hence thesis;

    end;

    

     Lm7: ( In (( 0. F_Rat ), F_Complex )) = ( 0. F_Complex ) & ( In (( 1. F_Rat ), F_Complex )) = ( 1. F_Complex ) & ( In (( 0. INT.Ring ), F_Complex )) = ( 0. F_Complex ) & ( In (( 1. INT.Ring ), F_Complex )) = ( 1. F_Complex ) by Lm5, Th3, Th4;

    theorem :: ALGNUM_1:5

    

     Th8: for x,y be Element of B, x1,y1 be Element of A st A is Subring of B & x = x1 & y = y1 holds (x + y) = (x1 + y1)

    proof

      let x,y be Element of B, x1,y1 be Element of A;

      assume A is Subring of B;

      then the addF of A = (the addF of B || the carrier of A) by C0SP1:def 3;

      hence thesis by FUNCT_1: 49, ZFMISC_1: 87;

    end;

    theorem :: ALGNUM_1:6

    

     Th9: for x,y be Element of B, x1,y1 be Element of A st A is Subring of B & x = x1 & y = y1 holds (x * y) = (x1 * y1)

    proof

      let x,y be Element of B, x1,y1 be Element of A;

      assume A is Subring of B;

      then the multF of A = (the multF of B || the carrier of A) by C0SP1:def 3;

      hence thesis by FUNCT_1: 49, ZFMISC_1: 87;

    end;

    registration

      let c be Complex;

      reduce ( In (c, F_Complex )) to c;

      reducibility

      proof

        c in COMPLEX by XCMPLX_0:def 2;

        then c is Element of F_Complex by COMPLFLD:def 1;

        hence thesis by SUBSET_1:def 8;

      end;

    end

    begin

    definition

      let A,B be Ring;

      let p be Polynomial of A;

      let x be Element of B;

      :: ALGNUM_1:def1

      func Ext_eval (p,x) -> Element of B means

      : Def1: ex F be FinSequence of B st it = ( Sum F) & ( len F) = ( len p) & for n be Element of NAT st n in ( dom F) holds (F . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1))));

      existence

      proof

        deffunc G( Nat) = (( In ((p . ($1 -' 1)),B)) * (( power B) . (x,($1 -' 1))));

        consider F be FinSequence of B such that

         A1: ( len F) = ( len p) and

         A2: for n be Nat st n in ( dom F) holds (F . n) = G(n) from FINSEQ_2:sch 1;

        take y = ( Sum F);

        take F;

        thus y = ( Sum F) & ( len F) = ( len p) by A1;

        let n be Element of NAT ;

        assume n in ( dom F);

        hence thesis by A2;

      end;

      uniqueness

      proof

        let y1,y2 be Element of B;

        given F1 be FinSequence of B such that

         A3: y1 = ( Sum F1) and

         A4: ( len F1) = ( len p) and

         A5: for n be Element of NAT st n in ( dom F1) holds (F1 . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1))));

        given F2 be FinSequence of B such that

         A6: y2 = ( Sum F2) and

         A7: ( len F2) = ( len p) and

         A8: for n be Element of NAT st n in ( dom F2) holds (F2 . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1))));

        

         A9: ( dom F1) = ( Seg ( len p)) by A4, FINSEQ_1:def 3;

        now

          let n be Nat;

          assume

           A10: n in ( dom F1);

          then

           A11: n in ( dom F2) by A7, A9, FINSEQ_1:def 3;

          

          thus (F1 . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A5, A10

          .= (F2 . n) by A8, A11;

        end;

        hence thesis by A3, A4, A6, A7, FINSEQ_2: 9;

      end;

    end

    theorem :: ALGNUM_1:7

    

     Th11: for n be Element of NAT , A,B be Ring, z be Element of A st A is Subring of B holds (( power B) . (( In (z,B)),n)) = ( In ((( power A) . (z,n)),B))

    proof

      let n be Element of NAT , A,B be Ring, z be Element of A;

      assume

       A0: A is Subring of B;

      then z is Element of B by Lm6;

      then

       A2: ( In (z,B)) = z by SUBSET_1:def 8;

      

       A3: ( 1_ A) = ( 1_ B) by A0, C0SP1:def 3;

      reconsider x = z as Element of B by A0, Lm6;

      (( power B) . (( In (z,B)),n)) = ( In ((( power A) . (z,n)),B))

      proof

        defpred P[ Nat] means (( power B) . (( In (z,B)),$1)) = ( In ((( power A) . (z,$1)),B));

        

         A5: P[ 0 ]

        proof

          

           A6: ( In (( 1. A),B)) = ( 1. B) by A0, Lm5;

          ( In ((( power A) . (z, 0 )),B)) = ( 1. B) by A3, GROUP_1:def 7, A6;

          hence thesis by A3, GROUP_1:def 7;

        end;

        

         A7: for m be Nat st P[m] holds P[(m + 1)]

        proof

          let m be Nat;

          assume

           A9: P[m];

          

           A10: (( power A) . (z,m)) is Element of B by A0, Lm6;

          

           A11: ( In ((( power A) . (z,m)),B)) = (( power A) . (z,m)) by A10, SUBSET_1:def 8;

          

           A12: (( power A) . (z,(m + 1))) is Element of B by A0, Lm6;

          (( power B) . (( In (z,B)),(m + 1))) = ((( power B) . (( In (z,B)),m)) * ( In (z,B))) by GROUP_1:def 7

          .= ((( power A) . (z,m)) * z) by A0, A11, A2, Th9, A9

          .= (( power A) . (z,(m + 1))) by GROUP_1:def 7

          .= ( In ((( power A) . (z,(m + 1))),B)) by A12, SUBSET_1:def 8;

          hence thesis;

        end;

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

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ALGNUM_1:8

    

     Th12: for x1,x2 be Element of A st A is Subring of B holds (( In (x1,B)) + ( In (x2,B))) = ( In ((x1 + x2),B))

    proof

      let x1,x2 be Element of A;

      assume

       A0: A is Subring of B;

      then x1 is Element of B by Lm6;

      then

       A2: ( In (x1,B)) = x1 by SUBSET_1:def 8;

      x2 is Element of B by A0, Lm6;

      then

       A4: ( In (x2,B)) = x2 by SUBSET_1:def 8;

      (x1 + x2) is Element of B by A0, Lm6;

      

      then ( In ((x1 + x2),B)) = (x1 + x2) by SUBSET_1:def 8

      .= (( In (x1,B)) + ( In (x2,B))) by A0, A2, A4, Th8;

      hence thesis;

    end;

    theorem :: ALGNUM_1:9

    

     Th13: for x1,x2 be Element of A st A is Subring of B holds (( In (x1,B)) * ( In (x2,B))) = ( In ((x1 * x2),B))

    proof

      let x1,x2 be Element of A;

      assume

       A0: A is Subring of B;

      then x1 is Element of B by Lm6;

      then

       A2: ( In (x1,B)) = x1 by SUBSET_1:def 8;

      x2 is Element of B by A0, Lm6;

      then

       A4: ( In (x2,B)) = x2 by SUBSET_1:def 8;

      (x1 * x2) is Element of B by A0, Lm6;

      

      then ( In ((x1 * x2),B)) = (x1 * x2) by SUBSET_1:def 8

      .= (( In (x1,B)) * ( In (x2,B))) by A0, A2, A4, Th9;

      hence thesis;

    end;

    theorem :: ALGNUM_1:10

    

     Th14: for F be FinSequence of A, G be FinSequence of B st A is Subring of B & F = G holds ( In (( Sum F),B)) = ( Sum G)

    proof

      let F be FinSequence of A, G be FinSequence of B;

      assume

       A0: A is Subring of B;

      defpred P[ Nat] means for F be FinSequence of A, G be FinSequence of B st ( len F) = $1 & F = G holds ( In (( Sum F),B)) = ( Sum G);

      

       P1: P[ 0 ]

      proof

        let F be FinSequence of A, G be FinSequence of B;

        assume

         A1: ( len F) = 0 & F = G;

        then

         A2: F = ( <*> the carrier of A);

        

         A3: G = ( <*> the carrier of B) by A1;

        ( In (( Sum F),B)) = ( In (( 0. A),B)) by A2, RLVECT_1: 43

        .= ( In (( 0. B),B)) by A0, C0SP1:def 3

        .= ( 0. B) by SUBSET_1:def 8

        .= ( Sum G) by A3, RLVECT_1: 43;

        hence thesis;

      end;

      

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

      proof

        let n be Nat;

        assume

         A4: P[n];

        let F be FinSequence of A, G be FinSequence of B;

        assume

         A5: ( len F) = (n + 1) & F = G;

        reconsider F0 = (F | n) as FinSequence of A;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then

         A6: (n + 1) in ( dom F) by A5, FINSEQ_1:def 3;

        ( rng F) c= the carrier of A;

        then

        reconsider af = (F . (n + 1)) as Element of A by A6, FUNCT_1: 3;

        

         A7: ( len F0) = n by FINSEQ_1: 59, A5, NAT_1: 11;

        

         A8: ( len F) = (( len F0) + 1) by A5, FINSEQ_1: 59, NAT_1: 11;

        

         A9: F0 = (F | ( dom F0)) by A7, FINSEQ_1:def 3;

        reconsider G0 = (G | n) as FinSequence of B;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then

         A10: (n + 1) in ( dom G) by A5, FINSEQ_1:def 3;

        ( rng G) c= the carrier of B;

        then

        reconsider bf = (G . (n + 1)) as Element of B by A10, FUNCT_1: 3;

        

         A11: ( len F0) = n & F0 = G0 by FINSEQ_1: 59, A5, NAT_1: 11;

        G = (G0 ^ <*bf*>) by A5, FINSEQ_3: 55;

        

        then ( Sum G) = (( Sum G0) + bf) by FVSUM_1: 71

        .= (( In (( Sum F0),B)) + bf) by A4, A11

        .= (( In (( Sum F0),B)) + ( In (af,B))) by A5, SUBSET_1:def 8

        .= ( In ((( Sum F0) + af),B)) by A0, Th12

        .= ( In (( Sum F),B)) by A5, A8, A9, RLVECT_1: 38;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: ALGNUM_1:11

    

     Th15: for n be Nat, x be Element of A, p be Polynomial of A st A is Subring of B holds (( In ((p . (n -' 1)),B)) * (( power B) . (( In (x,B)),(n -' 1)))) = ( In (((p . (n -' 1)) * (( power A) . (x,(n -' 1)))),B))

    proof

      let n be Nat, x be Element of A, p be Polynomial of A;

      assume

       A0: A is Subring of B;

      

      then ( In (((p . (n -' 1)) * (( power A) . (x,(n -' 1)))),B)) = (( In ((p . (n -' 1)),B)) * ( In ((( power A) . (x,(n -' 1))),B))) by Th13

      .= (( In ((p . (n -' 1)),B)) * (( power B) . (( In (x,B)),(n -' 1)))) by A0, Th11;

      hence thesis;

    end;

    theorem :: ALGNUM_1:12

    

     Th16: for x be Element of A, p be Polynomial of A st A is Subring of B holds ( Ext_eval (p,( In (x,B)))) = ( In (( eval (p,x)),B))

    proof

      let x be Element of A, p be Polynomial of A;

      assume

       A0: A is Subring of B;

      consider F1 be FinSequence of B such that

       A1: ( Ext_eval (p,( In (x,B)))) = ( Sum F1) and

       A2: ( len F1) = ( len p) and

       A3: for n be Element of NAT st n in ( dom F1) holds (F1 . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (( In (x,B)),(n -' 1)))) by Def1;

      consider F2 be FinSequence of A such that

       A4: ( eval (p,x)) = ( Sum F2) and

       A5: ( len F2) = ( len p) and

       A6: for n be Element of NAT st n in ( dom F2) holds (F2 . n) = ((p . (n -' 1)) * (( power A) . (x,(n -' 1)))) by POLYNOM4:def 2;

      F1 = F2

      proof

        

         A11: ( rng F2) c= the carrier of A;

        

         A8: ( dom F1) = ( dom F2) by A2, A5, FINSEQ_3: 29;

        for k be Nat st k in ( dom F1) holds (F1 . k) = (F2 . k)

        proof

          let k be Nat;

          assume

           A10: k in ( dom F1);

          then (F2 . k) is Element of A by A8, FUNCT_1: 3, A11;

          then

           A13: (F2 . k) is Element of B by A0, Lm6;

          (F1 . k) = (( In ((p . (k -' 1)),B)) * (( power B) . (( In (x,B)),(k -' 1)))) by A3, A10

          .= ( In (((p . (k -' 1)) * (( power A) . (x,(k -' 1)))),B)) by A0, Th15

          .= ( In ((F2 . k),B)) by A6, A10, A8

          .= (F2 . k) by A13, SUBSET_1:def 8;

          hence thesis;

        end;

        hence thesis by A2, A5, FINSEQ_3: 29;

      end;

      hence thesis by A1, A4, A0, Th14;

    end;

    theorem :: ALGNUM_1:13

    

     Th17: for x be Element of B holds ( Ext_eval (( 0_. A),x)) = ( 0. B)

    proof

      let x be Element of B;

      consider F be FinSequence of B such that

       A1: ( Ext_eval (( 0_. A),x)) = ( Sum F) and

       A2: ( len F) = ( len ( 0_. A)) and for n be Element of NAT st n in ( dom F) holds (F . n) = (( In ((( 0_. A) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      F = ( <*> the carrier of B) by A2, POLYNOM4: 3;

      hence thesis by A1, RLVECT_1: 43;

    end;

    theorem :: ALGNUM_1:14

    

     Th18: for A,B be non degenerated Ring holds for x be Element of B st A is Subring of B holds ( Ext_eval (( 1_. A),x)) = ( 1. B)

    proof

      let A,B be non degenerated Ring;

      let x be Element of B;

      assume

       A0: A is Subring of B;

      consider F be FinSequence of B such that

       A1: ( Ext_eval (( 1_. A),x)) = ( Sum F) and

       A2: ( len F) = ( len ( 1_. A)) and

       A3: for n be Element of NAT st n in ( dom F) holds (F . n) = (( In ((( 1_. A) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      ( len F) = 1 by A2, POLYNOM4: 4;

      

      then

       A4: (F . 1) = (( In ((( 1_. A) . (1 -' 1)),B)) * (( power B) . (x,(1 -' 1)))) by A3, FINSEQ_3: 25

      .= (( In ((( 1_. A) . 0 ),B)) * (( power B) . (x,(1 -' 1)))) by XREAL_1: 232

      .= (( In (( 1. A),B)) * (( power B) . (x,(1 -' 1)))) by POLYNOM3: 30

      .= (( 1. B) * (( power B) . (x,(1 -' 1)))) by A0, Lm5

      .= (( power B) . (x, 0 )) by XREAL_1: 232

      .= ( 1_ B) by GROUP_1:def 7

      .= ( 1. B);

      ( Sum F) = ( Sum <*( 1. B)*>) by A2, POLYNOM4: 4, FINSEQ_1: 40, A4

      .= ( 1. B) by RLVECT_1: 44;

      hence thesis by A1;

    end;

    theorem :: ALGNUM_1:15

    

     Th19: for x be Element of B, p,q be Polynomial of A st A is Subring of B holds ( Ext_eval ((p + q),x)) = (( Ext_eval (p,x)) + ( Ext_eval (q,x)))

    proof

      let x be Element of B, p,q be Polynomial of A;

      assume

       A0: A is Subring of B;

      reconsider k = ( max (( len p),( len q))) as Element of NAT ;

      

       A1: (k - ( len p)) >= 0 by XREAL_1: 48, XXREAL_0: 25;

      consider F1 be FinSequence of B such that

       A2: ( Ext_eval (p,x)) = ( Sum F1) and

       A3: ( len F1) = ( len p) and

       A4: for n be Element of NAT st n in ( dom F1) holds (F1 . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      

       A5: ( len (F1 ^ ((k -' ( len F1)) |-> ( 0. B)))) = (( len p) + ( len ((k -' ( len p)) |-> ( 0. B)))) by A3, FINSEQ_1: 22

      .= (( len p) + (k -' ( len p))) by CARD_1:def 7

      .= (( len p) + (k - ( len p))) by A1, XREAL_0:def 2

      .= k;

      

       A6: (k - ( len q)) >= 0 by XREAL_1: 48, XXREAL_0: 25;

      k >= ( len p) & k >= ( len q) by XXREAL_0: 25;

      then

       A7: (k - ( len (p + q))) >= 0 by POLYNOM4: 6, XREAL_1: 48;

      consider F3 be FinSequence of B such that

       A8: ( Ext_eval ((p + q),x)) = ( Sum F3) and

       A9: ( len F3) = ( len (p + q)) and

       A10: for n be Element of NAT st n in ( dom F3) holds (F3 . n) = (( In (((p + q) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      

       A11: ( len (F3 ^ ((k -' ( len F3)) |-> ( 0. B)))) = (( len F3) + ( len ((k -' ( len F3)) |-> ( 0. B)))) by FINSEQ_1: 22

      .= (( len (p + q)) + (k -' ( len (p + q)))) by CARD_1:def 7, A9

      .= (( len (p + q)) + (k - ( len (p + q)))) by A7, XREAL_0:def 2

      .= k;

      consider F2 be FinSequence of B such that

       A12: ( Ext_eval (q,x)) = ( Sum F2) and

       A13: ( len F2) = ( len q) and

       A14: for n be Element of NAT st n in ( dom F2) holds (F2 . n) = (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      ( len (F2 ^ ((k -' ( len F2)) |-> ( 0. B)))) = (( len q) + ( len ((k -' ( len q)) |-> ( 0. B)))) by A13, FINSEQ_1: 22

      .= (( len q) + (k -' ( len q))) by CARD_1:def 7

      .= (( len q) + (k - ( len q))) by A6, XREAL_0:def 2

      .= k;

      then

      reconsider G1 = (F1 ^ ((k -' ( len F1)) |-> ( 0. B))), G2 = (F2 ^ ((k -' ( len F2)) |-> ( 0. B))), G3 = (F3 ^ ((k -' ( len F3)) |-> ( 0. B))) as Element of (k -tuples_on the carrier of B) by A5, A11, FINSEQ_2: 92;

      now

        let n be Nat;

        assume

         A15: n in ( Seg k);

        then

         A16: ( 0 + 1) <= n by FINSEQ_1: 1;

        

         A17: n <= k by A15, FINSEQ_1: 1;

        per cases by XXREAL_0: 1;

          suppose

           A18: ( len p) > ( len q);

          then k = ( len p) by XXREAL_0:def 10;

          then ( len (p + q)) = ( len p) by A18, POLYNOM4: 7;

          then

           A20: n in ( dom F3) by A9, A15, A18, XXREAL_0:def 10, FINSEQ_1:def 3;

          

           A21: ( len G2) = k by CARD_1:def 7;

          then

           A22: n in ( dom G2) by A15, FINSEQ_1:def 3;

          then

           A23: (G2 /. n) = (G2 . n) by PARTFUN1:def 6;

          ( len G1) = k by CARD_1:def 7;

          then

           A24: n in ( dom G1) by A15, FINSEQ_1:def 3;

          then

           A25: (G1 /. n) = (G1 . n) by PARTFUN1:def 6;

          

           A26: n in ( dom F1) by A3, A15, A18, XXREAL_0:def 10, FINSEQ_1:def 3;

          

           A27: (G1 /. n) = (G1 . n) by A24, PARTFUN1:def 6

          .= (F1 . n) by A26, FINSEQ_1:def 7

          .= (F1 /. n) by A26, PARTFUN1:def 6;

          

           A28: (F1 . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A4, A26;

          now

            per cases ;

              suppose n <= ( len q);

              then

               A29: n in ( dom F2) by A16, A13, FINSEQ_3: 25;

              then

               A30: (F2 . n) = (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A14;

              

               A31: (G2 /. n) = (G2 . n) by A22, PARTFUN1:def 6

              .= (F2 . n) by A29, FINSEQ_1:def 7

              .= (F2 /. n) by A29, PARTFUN1:def 6;

              

              thus (G3 . n) = (F3 . n) by A20, FINSEQ_1:def 7

              .= (( In (((p + q) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A10, A20

              .= (( In (((p . (n -' 1)) + (q . (n -' 1))),B)) * (( power B) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= ((( In ((p . (n -' 1)),B)) + ( In ((q . (n -' 1)),B))) * (( power B) . (x,(n -' 1)))) by A0, Th12

              .= ((( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) + (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1))))) by VECTSP_1:def 3

              .= ((( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) + (F2 /. n)) by A29, A30, PARTFUN1:def 6

              .= ((F1 /. n) + (F2 /. n)) by A26, A28, PARTFUN1:def 6

              .= ((G1 + G2) . n) by A15, A25, A23, A27, A31, FVSUM_1: 18;

            end;

              suppose

               A32: n > ( len q);

              then

               A33: n >= (( len q) + 1) by NAT_1: 13;

              then (n - 1) >= ( len q) by XREAL_1: 19;

              then

               A34: (n -' 1) >= ( len q) by XREAL_0:def 2;

              (n - ( len F2)) <= (k - ( len F2)) by A17, XREAL_1: 9;

              then

               A35: (n - ( len F2)) <= (k -' ( len F2)) by XREAL_0:def 2;

              

               A36: (n - ( len F2)) >= 1 by A13, A33, XREAL_1: 19;

              then (n - ( len F2)) = (n -' ( len F2)) by XREAL_0:def 2;

              then

               A37: (n - ( len F2)) in ( Seg (k -' ( len F2))) by A36, A35;

              n <= ( len G2) by A15, A21, FINSEQ_1: 1;

              

              then

               A38: (G2 /. n) = (((k -' ( len F2)) |-> ( 0. B)) . (n - ( len F2))) by A13, A23, A32, FINSEQ_1: 24

              .= ( 0. B) by A37, FUNCOP_1: 7;

              

              thus (G3 . n) = (F3 . n) by A20, FINSEQ_1:def 7

              .= (( In (((p + q) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A10, A20

              .= (( In (((p . (n -' 1)) + (q . (n -' 1))),B)) * (( power B) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= (( In (((p . (n -' 1)) + ( 0. A)),B)) * (( power B) . (x,(n -' 1)))) by A34, ALGSEQ_1: 8

              .= (F1 . n) by A4, A26

              .= ((G1 /. n) + ( 0. B)) by A26, A27, PARTFUN1:def 6

              .= ((G1 + G2) . n) by A15, A25, A23, A38, FVSUM_1: 18;

            end;

          end;

          hence (G3 . n) = ((G1 + G2) . n);

        end;

          suppose

           A39: ( len p) < ( len q);

          then k = ( len q) by XXREAL_0:def 10;

          then ( len (p + q)) = ( len q) by A39, POLYNOM4: 7;

          then

           A41: n in ( dom F3) by A9, A15, A39, XXREAL_0:def 10, FINSEQ_1:def 3;

          

           A42: ( len G1) = k by CARD_1:def 7;

          then

           A43: n in ( dom G1) by A15, FINSEQ_1:def 3;

          then

           A44: (G1 /. n) = (G1 . n) by PARTFUN1:def 6;

          ( len G2) = k by CARD_1:def 7;

          then

           A45: n in ( dom G2) by A15, FINSEQ_1:def 3;

          then

           A46: (G2 /. n) = (G2 . n) by PARTFUN1:def 6;

          

           A47: n in ( dom F2) by A13, A15, A39, XXREAL_0:def 10, FINSEQ_1:def 3;

          

           A48: (G2 /. n) = (G2 . n) by A45, PARTFUN1:def 6

          .= (F2 . n) by A47, FINSEQ_1:def 7

          .= (F2 /. n) by A47, PARTFUN1:def 6;

          

           A49: (F2 . n) = (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A14, A47;

          now

            per cases ;

              suppose n <= ( len p);

              then

               A50: n in ( dom F1) by A16, A3, FINSEQ_3: 25;

              then

               A51: (F1 . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A4;

              

               A52: (G1 /. n) = (G1 . n) by A43, PARTFUN1:def 6

              .= (F1 . n) by A50, FINSEQ_1:def 7

              .= (F1 /. n) by A50, PARTFUN1:def 6;

              

              thus (G3 . n) = (F3 . n) by A41, FINSEQ_1:def 7

              .= (( In (((p + q) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A10, A41

              .= (( In (((p . (n -' 1)) + (q . (n -' 1))),B)) * (( power B) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= ((( In ((p . (n -' 1)),B)) + ( In ((q . (n -' 1)),B))) * (( power B) . (x,(n -' 1)))) by A0, Th12

              .= ((( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) + (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1))))) by VECTSP_1:def 3

              .= ((F1 /. n) + (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1))))) by A50, A51, PARTFUN1:def 6

              .= ((F1 /. n) + (F2 /. n)) by A47, A49, PARTFUN1:def 6

              .= ((G1 + G2) . n) by A15, A44, A46, A48, A52, FVSUM_1: 18;

            end;

              suppose

               A53: n > ( len p);

              then

               A54: n >= (( len p) + 1) by NAT_1: 13;

              then (n - 1) >= ( len p) by XREAL_1: 19;

              then

               A55: (n -' 1) >= ( len p) by XREAL_0:def 2;

              (n - ( len F1)) <= (k - ( len F1)) by A17, XREAL_1: 9;

              then

               A56: (n - ( len F1)) <= (k -' ( len F1)) by XREAL_0:def 2;

              

               A57: (n - ( len F1)) >= 1 by A3, A54, XREAL_1: 19;

              then (n - ( len F1)) = (n -' ( len F1)) by XREAL_0:def 2;

              then

               A58: (n - ( len F1)) in ( Seg (k -' ( len F1))) by A57, A56;

              n <= ( len G1) by A15, A42, FINSEQ_1: 1;

              

              then

               A59: (G1 /. n) = (((k -' ( len F1)) |-> ( 0. B)) . (n - ( len F1))) by A3, A44, A53, FINSEQ_1: 24

              .= ( 0. B) by A58, FUNCOP_1: 7;

              

              thus (G3 . n) = (F3 . n) by A41, FINSEQ_1:def 7

              .= (( In (((p + q) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A10, A41

              .= (( In (((p . (n -' 1)) + (q . (n -' 1))),B)) * (( power B) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= (( In ((( 0. A) + (q . (n -' 1))),B)) * (( power B) . (x,(n -' 1)))) by A55, ALGSEQ_1: 8

              .= (F2 . n) by A14, A47

              .= (( 0. B) + (G2 /. n)) by A47, A48, PARTFUN1:def 6

              .= ((G1 + G2) . n) by A15, A44, A46, A59, FVSUM_1: 18;

            end;

          end;

          hence (G3 . n) = ((G1 + G2) . n);

        end;

          suppose

           A60: ( len p) = ( len q);

          ( len G2) = k by CARD_1:def 7;

          then

           A61: n in ( dom G2) by A15, FINSEQ_1:def 3;

          then

           A62: (G2 /. n) = (G2 . n) by PARTFUN1:def 6;

          ( len G1) = k by CARD_1:def 7;

          then

           A63: n in ( dom G1) by A15, FINSEQ_1:def 3;

          then

           A64: (G1 /. n) = (G1 . n) by PARTFUN1:def 6;

          

           A65: ( len G3) = k by CARD_1:def 7;

          

           A66: n in ( dom F2) by A13, A15, A60, FINSEQ_1:def 3;

          

           A67: n in ( dom F1) by A3, A15, A60, FINSEQ_1:def 3;

          then

           A68: (F1 . n) = (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A4;

          

           A69: (G1 /. n) = (G1 . n) by A63, PARTFUN1:def 6

          .= (F1 . n) by A67, FINSEQ_1:def 7

          .= (F1 /. n) by A67, PARTFUN1:def 6;

          now

            per cases ;

              suppose

               A70: n <= ( len (p + q));

              

               A71: n in ( dom F2) by A13, A15, A60, FINSEQ_1:def 3;

              then

               A72: (F2 . n) = (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A14;

              

               A73: (G2 /. n) = (G2 . n) by A61, PARTFUN1:def 6

              .= (F2 . n) by A71, FINSEQ_1:def 7

              .= (F2 /. n) by A71, PARTFUN1:def 6;

              n in ( Seg ( len (p + q))) by A16, A70;

              then

               A74: n in ( dom F3) by A9, FINSEQ_1:def 3;

              

              hence (G3 . n) = (F3 . n) by FINSEQ_1:def 7

              .= (( In (((p + q) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A10, A74

              .= (( In (((p . (n -' 1)) + (q . (n -' 1))),B)) * (( power B) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= ((( In ((p . (n -' 1)),B)) + ( In ((q . (n -' 1)),B))) * (( power B) . (x,(n -' 1)))) by A0, Th12

              .= ((( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) + (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1))))) by VECTSP_1:def 3

              .= ((( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) + (F2 /. n)) by A71, A72, PARTFUN1:def 6

              .= ((F1 /. n) + (F2 /. n)) by A67, A68, PARTFUN1:def 6

              .= ((G1 + G2) . n) by A15, A64, A62, A69, A73, FVSUM_1: 18;

            end;

              suppose

               A75: n > ( len (p + q));

              then

               A76: n >= (( len (p + q)) + 1) by NAT_1: 13;

              then (n - 1) >= ((( len (p + q)) + 1) - 1) by XREAL_1: 9;

              then

               A77: (n -' 1) >= ( len (p + q)) by XREAL_0:def 2;

              (n - ( len F3)) <= (k - ( len F3)) by A17, XREAL_1: 9;

              then

               A78: (n - ( len F3)) <= (k -' ( len F3)) by XREAL_0:def 2;

              

               A79: (G2 . n) = (F2 . n) by A66, FINSEQ_1:def 7

              .= (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A14, A66;

              

               A80: (G1 . n) = (F1 . n) by A67, FINSEQ_1:def 7

              .= (( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A4, A67;

              

               A81: (n - ( len F3)) >= 1 by A9, A76, XREAL_1: 19;

              then (n - ( len F3)) = (n -' ( len F3)) by XREAL_0:def 2;

              then

               A82: (n - ( len F3)) in ( Seg (k -' ( len F3))) by A81, A78;

              n <= ( len G3) by A15, A65, FINSEQ_1: 1;

              

              hence (G3 . n) = (((k -' ( len F3)) |-> ( 0. B)) . (n - ( len F3))) by A9, A75, FINSEQ_1: 24

              .= (( 0. B) * (( power B) . (x,(n -' 1)))) by A82, FUNCOP_1: 7

              .= (( In (( 0. A),B)) * (( power B) . (x,(n -' 1)))) by A0, Lm5

              .= (( In (((p + q) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by A77, ALGSEQ_1: 8

              .= (( In (((p . (n -' 1)) + (q . (n -' 1))),B)) * (( power B) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= ((( In ((p . (n -' 1)),B)) + ( In ((q . (n -' 1)),B))) * (( power B) . (x,(n -' 1)))) by A0, Th12

              .= ((( In ((p . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) + (( In ((q . (n -' 1)),B)) * (( power B) . (x,(n -' 1))))) by VECTSP_1:def 3

              .= ((G1 + G2) . n) by A15, A80, A79, FVSUM_1: 18;

            end;

          end;

          hence (G3 . n) = ((G1 + G2) . n);

        end;

      end;

      then

       A83: G3 = (G1 + G2) by FINSEQ_2: 119;

      

       A84: ( Sum G3) = (( Sum F3) + ( Sum ((k -' ( len F3)) |-> ( 0. B)))) by RLVECT_1: 41

      .= (( Sum F3) + ( 0. B)) by MATRIX_3: 11

      .= ( Sum F3);

      

       A85: ( Sum G2) = (( Sum F2) + ( Sum ((k -' ( len F2)) |-> ( 0. B)))) by RLVECT_1: 41

      .= (( Sum F2) + ( 0. B)) by MATRIX_3: 11

      .= ( Sum F2);

      ( Sum G1) = (( Sum F1) + ( Sum ((k -' ( len F1)) |-> ( 0. B)))) by RLVECT_1: 41

      .= (( Sum F1) + ( 0. B)) by MATRIX_3: 11

      .= ( Sum F1);

      hence thesis by A2, A12, A8, A85, A84, A83, FVSUM_1: 76;

    end;

    theorem :: ALGNUM_1:16

    

     Th20: for p,q be Polynomial of A st A is Subring of B & ( len p) > 0 & ( len q) > 0 holds for x be Element of B holds ( Ext_eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = (( In (((p . (( len p) -' 1)) * (q . (( len q) -' 1))),B)) * (( power B) . (x,((( len p) + ( len q)) -' 2))))

    proof

      let p,q be Polynomial of A;

      assume that

       A0: A is Subring of B and

       A1: ( len p) > 0 and

       A2: ( len q) > 0 ;

      

       A3: ( len q) >= ( 0 + 1) by A2, NAT_1: 13;

      

       A5: ( len p) >= ( 0 + 1) by A1, NAT_1: 13;

      

       A6: (( len p) - 1) = (( len p) -' 1) by A1, XREAL_0:def 2;

      

       A7: (( len p) + ( len q)) >= ( 0 + (1 + 1)) by A5, A3, XREAL_1: 7;

      reconsider i1 = ((( len p) + ( len q)) - 1) as Element of NAT by A1, INT_1: 3;

      

       A9: ((i1 -' 1) + 1) = i1 by A7, XREAL_1: 19, XREAL_1: 235;

      set LMp = ( Leading-Monomial p), LMq = ( Leading-Monomial q);

      let x be Element of B;

      consider F be FinSequence of B such that

       A10: ( Ext_eval ((LMp *' LMq),x)) = ( Sum F) and

       A11: ( len F) = ( len (LMp *' LMq)) and

       A12: for n be Element of NAT st n in ( dom F) holds (F . n) = (( In (((LMp *' LMq) . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      consider r be FinSequence of A such that

       A13: ( len r) = ((i1 -' 1) + 1) and

       A14: ((LMp *' LMq) . (i1 -' 1)) = ( Sum r) and

       A15: for k be Element of NAT st k in ( dom r) holds (r . k) = ((LMp . (k -' 1)) * (LMq . (((i1 -' 1) + 1) -' k))) by POLYNOM3:def 9;

      (( len p) + 0 ) <= (( len p) + (( len q) - 1)) by A2, XREAL_1: 7;

      then ( len p) in ( Seg ( len r)) by A5, A9, A13;

      then

       A16: ( len p) in ( dom r) by FINSEQ_1:def 3;

      (i1 -' ( len p)) = ((( len p) + (( len q) - 1)) - ( len p)) by A2, XREAL_0:def 2

      .= (( len q) -' 1) by A2, XREAL_0:def 2;

      then

       A17: (r . ( len p)) = ((LMp . (( len p) -' 1)) * (LMq . (( len q) -' 1))) by A9, A15, A16;

      now

        let i be Element of NAT ;

        assume that

         A18: i in ( dom r) and

         A19: i <> ( len p);

        i >= ( 0 + 1) by A18, FINSEQ_3: 25;

        then (i -' 1) = (i - 1) by XREAL_0:def 2;

        then

         A20: (i -' 1) <> (( len p) -' 1) by A6, A19;

        

        thus (r /. i) = (r . i) by A18, PARTFUN1:def 6

        .= ((LMp . (i -' 1)) * (LMq . (((i1 -' 1) + 1) -' i))) by A15, A18

        .= (( 0. A) * (LMq . (((i1 -' 1) + 1) -' i))) by A20, POLYNOM4:def 1

        .= ( 0. A);

      end;

      

      then

       A21: ( Sum r) = (r /. ( len p)) by A16, POLYNOM2: 3

      .= ((LMp . (( len p) -' 1)) * (LMq . (( len q) -' 1))) by A16, A17, PARTFUN1:def 6

      .= ((p . (( len p) -' 1)) * (LMq . (( len q) -' 1))) by POLYNOM4:def 1

      .= ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) by POLYNOM4:def 1;

      

       A22: (( len q) - 1) = (( len q) -' 1) by A2, XREAL_0:def 2;

       A23:

      now

        let i be Element of NAT ;

        assume that

         A24: i in ( dom F) and

         A25: i <> i1;

        consider r1 be FinSequence of A such that

         A26: ( len r1) = ((i -' 1) + 1) and

         A27: ((LMp *' LMq) . (i -' 1)) = ( Sum r1) and

         A28: for k be Element of NAT st k in ( dom r1) holds (r1 . k) = ((LMp . (k -' 1)) * (LMq . (((i -' 1) + 1) -' k))) by POLYNOM3:def 9;

        

         A29: ((i -' 1) + 1) = i by A24, FINSEQ_3: 25, XREAL_1: 235;

         A30:

        now

          let j be Element of NAT ;

          assume

           A31: j in ( dom r1);

          then j >= ( 0 + 1) by FINSEQ_3: 25;

          then

           A32: (j -' 1) = (j - 1) by XREAL_0:def 2;

          per cases ;

            suppose j <> ( len p);

            then

             A33: (j -' 1) <> (( len p) -' 1) by A6, A32;

            

            thus (r1 . j) = ((LMp . (j -' 1)) * (LMq . (((i -' 1) + 1) -' j))) by A28, A31

            .= (( 0. A) * (LMq . (((i -' 1) + 1) -' j))) by A33, POLYNOM4:def 1

            .= ( 0. A);

          end;

            suppose

             A34: j = ( len p);

            j in ( Seg ( len r1)) by A31, FINSEQ_1:def 3;

            then i >= ( 0 + j) by A26, A29, FINSEQ_1: 1;

            then (i -' ( len p)) = (i - ( len p)) by A34, XREAL_1: 19, XREAL_0:def 2;

            then

             A35: (i -' ( len p)) <> (( len q) -' 1) by A22, A25;

            

            thus (r1 . j) = ((LMp . (j -' 1)) * (LMq . (i -' ( len p)))) by A28, A29, A31, A34

            .= ((LMp . (j -' 1)) * ( 0. A)) by A35, POLYNOM4:def 1

            .= ( 0. A);

          end;

        end;

        

        thus (F /. i) = (F . i) by A24, PARTFUN1:def 6

        .= (( In (( Sum r1),B)) * (( power B) . (x,(i -' 1)))) by A12, A24, A27

        .= (( In (( 0. A),B)) * (( power B) . (x,(i -' 1)))) by A30, POLYNOM3: 1

        .= (( 0. B) * (( power B) . (x,(i -' 1)))) by A0, Lm5

        .= ( 0. B);

      end;

      

       A36: ((( len p) + ( len q)) - 2) >= 0 by A7, XREAL_1: 19;

      ((( len p) + ( len q)) - (1 + 1)) >= 0 by A7, XREAL_1: 19;

      

      then

       A37: (i1 -' 1) = (((( len p) + ( len q)) - 1) - 1) by XREAL_0:def 2

      .= ((( len p) + ( len q)) -' 2) by A36, XREAL_0:def 2;

      per cases ;

        suppose ((LMp *' LMq) . (i1 -' 1)) <> ( 0. A);

        then ( len F) >= i1 by A11, ALGSEQ_1: 8, A9, NAT_1: 13;

        then

         A38: i1 in ( dom F) by A7, XREAL_1: 19, FINSEQ_3: 25;

        

        hence ( Ext_eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = (F /. i1) by A10, A23, POLYNOM2: 3

        .= (F . i1) by A38, PARTFUN1:def 6

        .= (( In (((p . (( len p) -' 1)) * (q . (( len q) -' 1))),B)) * (( power B) . (x,((( len p) + ( len q)) -' 2)))) by A12, A14, A37, A21, A38;

      end;

        suppose

         A39: ((LMp *' LMq) . (i1 -' 1)) = ( 0. A);

        now

          let j be Nat;

          assume j >= 0 ;

          j in NAT by ORDINAL1:def 12;

          then

          consider r1 be FinSequence of A such that

           A40: ( len r1) = (j + 1) and

           A41: ((LMp *' LMq) . j) = ( Sum r1) and

           A42: for k be Element of NAT st k in ( dom r1) holds (r1 . k) = ((LMp . (k -' 1)) * (LMq . ((j + 1) -' k))) by POLYNOM3:def 9;

          now

            per cases ;

              suppose j = (i1 -' 1);

              hence ((LMp *' LMq) . j) = ( 0. A) by A39;

            end;

              suppose

               A43: j <> (i1 -' 1);

              now

                let k be Element of NAT ;

                assume

                 A44: k in ( dom r1);

                per cases ;

                  suppose

                   A45: (k -' 1) <> (( len p) -' 1);

                  

                  thus (r1 . k) = ((LMp . (k -' 1)) * (LMq . ((j + 1) -' k))) by A42, A44

                  .= (( 0. A) * (LMq . ((j + 1) -' k))) by A45, POLYNOM4:def 1

                  .= ( 0. A);

                end;

                  suppose

                   A46: (k -' 1) = (( len p) -' 1);

                  

                   A47: k in ( Seg ( len r1)) by A44, FINSEQ_1:def 3;

                  ( 0 + 1) <= k by A44, FINSEQ_3: 25;

                  then

                   A48: (k -' 1) = (k - 1) by XREAL_0:def 2;

                  ( 0 + k) <= (j + 1) by A40, A47, FINSEQ_1: 1;

                  then ((j + 1) - k) >= 0 by XREAL_1: 19;

                  then

                   A49: ((j + 1) -' k) = ((j - ( len p)) + 1) by A6, A46, A48, XREAL_0:def 2;

                  

                   A50: ((j - ( len p)) + 1) <> (((i1 -' 1) - ( len p)) + 1) by A43;

                  

                  thus (r1 . k) = ((LMp . (k -' 1)) * (LMq . ((j + 1) -' k))) by A42, A44

                  .= ((LMp . (k -' 1)) * ( 0. A)) by A22, A9, A49, A50, POLYNOM4:def 1

                  .= ( 0. A);

                end;

              end;

              hence ((LMp *' LMq) . j) = ( 0. A) by A41, POLYNOM3: 1;

            end;

          end;

          hence ((LMp *' LMq) . j) = ( 0. A);

        end;

        then 0 is_at_least_length_of (LMp *' LMq);

        then ( len (LMp *' LMq)) = 0 by ALGSEQ_1:def 3;

        then

         A52: (LMp *' LMq) = ( 0_. A) by POLYNOM4: 5;

        ( 0. B) = ( In (((p . (( len p) -' 1)) * (q . (( len q) -' 1))),B)) by A0, Lm5, A21, A14, A39;

        hence thesis by Th17, A52;

      end;

    end;

    theorem :: ALGNUM_1:17

    

     Th21: for p be Polynomial of A holds for x be Element of B st A is Subring of B holds ( Ext_eval (( Leading-Monomial p),x)) = (( In ((p . (( len p) -' 1)),B)) * (( power B) . (x,(( len p) -' 1))))

    proof

      let p be Polynomial of A;

      let x be Element of B;

      assume

       A0: A is Subring of B;

      set LMp = ( Leading-Monomial p);

      consider F be FinSequence of B such that

       A1: ( Ext_eval (LMp,x)) = ( Sum F) and

       A2: ( len F) = ( len LMp) and

       A3: for n be Element of NAT st n in ( dom F) holds (F . n) = (( In ((LMp . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      

       A4: ( len F) = ( len p) by A2, POLYNOM4: 15;

      per cases ;

        suppose

         A5: ( len p) > 0 ;

        then

         A7: ( len p) >= ( 0 + 1) by NAT_1: 13;

        then

         A6: ( len p) in ( dom F) by A4, FINSEQ_3: 25;

        now

          

           A8: (( len p) -' 1) = (( len p) - 1) by A5, XREAL_0:def 2;

          let i be Element of NAT ;

          assume that

           A9: i in ( dom F) and

           A10: i <> ( len p);

          i >= ( 0 + 1) by A9, FINSEQ_3: 25;

          then (i -' 1) = (i - 1) by XREAL_0:def 2;

          then

           A11: (i -' 1) <> (( len p) -' 1) by A10, A8;

          

          thus (F /. i) = (F . i) by A9, PARTFUN1:def 6

          .= (( In ((LMp . (i -' 1)),B)) * (( power B) . (x,(i -' 1)))) by A3, A9

          .= (( In (( 0. A),B)) * (( power B) . (x,(i -' 1)))) by A11, POLYNOM4:def 1

          .= (( 0. B) * (( power B) . (x,(i -' 1)))) by A0, Lm5

          .= ( 0. B);

        end;

        

        then ( Sum F) = (F /. ( len p)) by A4, A7, FINSEQ_3: 25, POLYNOM2: 3

        .= (F . ( len p)) by A6, PARTFUN1:def 6

        .= (( In ((LMp . (( len p) -' 1)),B)) * (( power B) . (x,(( len p) -' 1)))) by A3, A7, A4, FINSEQ_3: 25;

        hence thesis by A1, POLYNOM4:def 1;

      end;

        suppose

         A12: ( len p) = 0 ;

        then

         A13: p = ( 0_. A) by POLYNOM4: 5;

        LMp = ( 0_. A) by A12, POLYNOM4: 12;

        

        hence ( Ext_eval (( Leading-Monomial p),x)) = (( 0. B) * (( power B) . (x,(( len p) -' 1)))) by Th17

        .= (( In (( 0. A),B)) * (( power B) . (x,(( len p) -' 1)))) by A0, Lm5

        .= (( In ((p . (( len p) -' 1)),B)) * (( power B) . (x,(( len p) -' 1)))) by A13, FUNCOP_1: 7;

      end;

    end;

    theorem :: ALGNUM_1:18

    

     Th22: for B be comRing holds for p,q be Polynomial of A holds for x be Element of B st A is Subring of B holds ( Ext_eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = (( Ext_eval (( Leading-Monomial p),x)) * ( Ext_eval (( Leading-Monomial q),x)))

    proof

      let B be comRing;

      let p,q be Polynomial of A;

      let x be Element of B;

      assume

       A0: A is Subring of B;

      per cases ;

        suppose

         A1: ( len p) <> 0 & ( len q) <> 0 ;

        then

         A2: ( len q) >= ( 0 + 1) & ( len p) >= ( 0 + 1) by NAT_1: 13;

        

         A3: (( len q) - 1) = (( len q) -' 1) & (( len p) - 1) = (( len p) -' 1) by A1, XREAL_0:def 2;

        (( len p) + ( len q)) >= ( 0 + (1 + 1)) by A2, XREAL_1: 7;

        then

         A4: ((( len p) + ( len q)) -' 2) = ((( len p) + ( len q)) - 2) by XREAL_1: 19, XREAL_0:def 2;

        

         A5: ((( len p) + ( len q)) - (1 + 1)) = ((( len p) - 1) + (( len q) - 1));

        

        thus ( Ext_eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = (( In (((p . (( len p) -' 1)) * (q . (( len q) -' 1))),B)) * (( power B) . (x,((( len p) + ( len q)) -' 2)))) by A0, A1, Th20

        .= (( In (((p . (( len p) -' 1)) * (q . (( len q) -' 1))),B)) * ((( power B) . (x,(( len p) -' 1))) * (( power B) . (x,(( len q) -' 1))))) by A3, A4, A5, POLYNOM2: 1

        .= ((( In ((p . (( len p) -' 1)),B)) * ( In ((q . (( len q) -' 1)),B))) * ((( power B) . (x,(( len p) -' 1))) * (( power B) . (x,(( len q) -' 1))))) by A0, Th13

        .= (( In ((p . (( len p) -' 1)),B)) * (( In ((q . (( len q) -' 1)),B)) * ((( power B) . (x,(( len p) -' 1))) * (( power B) . (x,(( len q) -' 1)))))) by GROUP_1:def 3

        .= (( In ((p . (( len p) -' 1)),B)) * ((( power B) . (x,(( len p) -' 1))) * (( In ((q . (( len q) -' 1)),B)) * (( power B) . (x,(( len q) -' 1)))))) by GROUP_1:def 3

        .= ((( In ((p . (( len p) -' 1)),B)) * (( power B) . (x,(( len p) -' 1)))) * (( In ((q . (( len q) -' 1)),B)) * (( power B) . (x,(( len q) -' 1))))) by GROUP_1:def 3

        .= ((( In ((p . (( len p) -' 1)),B)) * (( power B) . (x,(( len p) -' 1)))) * ( Ext_eval (( Leading-Monomial q),x))) by A0, Th21

        .= (( Ext_eval (( Leading-Monomial p),x)) * ( Ext_eval (( Leading-Monomial q),x))) by A0, Th21;

      end;

        suppose ( len p) = 0 ;

        then

         A6: ( Leading-Monomial p) = ( 0_. A) by POLYNOM4: 12;

        

        hence ( Ext_eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = ( Ext_eval (( 0_. A),x)) by POLYNOM4: 2

        .= (( 0. B) * ( Ext_eval (( Leading-Monomial q),x))) by Th17

        .= (( Ext_eval (( Leading-Monomial p),x)) * ( Ext_eval (( Leading-Monomial q),x))) by A6, Th17;

      end;

        suppose ( len q) = 0 ;

        then ( len ( Leading-Monomial q)) = 0 by POLYNOM4: 15;

        then

         A7: ( Leading-Monomial q) = ( 0_. A) by POLYNOM4: 5;

        

        hence ( Ext_eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = ( Ext_eval (( 0_. A),x)) by POLYNOM3: 34

        .= (( Ext_eval (( Leading-Monomial p),x)) * ( 0. B)) by Th17

        .= (( Ext_eval (( Leading-Monomial p),x)) * ( Ext_eval (( Leading-Monomial q),x))) by A7, Th17;

      end;

    end;

    theorem :: ALGNUM_1:19

    

     Th15: for B be comRing holds for p,q be Polynomial of A holds for x be Element of B st A is Subring of B holds ( Ext_eval ((( Leading-Monomial p) *' q),x)) = (( Ext_eval (( Leading-Monomial p),x)) * ( Ext_eval (q,x)))

    proof

      let B be comRing;

      let p1,q be Polynomial of A;

      let x be Element of B;

      assume

       A0: A is Subring of B;

      set p = ( Leading-Monomial p1);

      defpred P[ Nat] means for q be Polynomial of A holds ( len q) = $1 implies ( Ext_eval ((p *' q),x)) = (( Ext_eval (p,x)) * ( Ext_eval (q,x)));

      

       A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]

      proof

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds for q be Polynomial of A holds ( len q) = n implies ( Ext_eval ((p *' q),x)) = (( Ext_eval (p,x)) * ( Ext_eval (q,x)));

        let q be Polynomial of A;

        assume

         A3: ( len q) = k;

        per cases ;

          suppose

           A4: ( len q) <> 0 ;

          set LMq = ( Leading-Monomial q);

          consider r be Polynomial of A such that

           A5: ( len r) < ( len q) and

           A6: q = (r + ( Leading-Monomial q)) and for n be Element of NAT st n < (( len q) - 1) holds (r . n) = (q . n) by A4, POLYNOM4: 16;

          

          thus ( Ext_eval ((p *' q),x)) = ( Ext_eval (((p *' r) + (p *' LMq)),x)) by A6, POLYNOM3: 31

          .= (( Ext_eval ((p *' r),x)) + ( Ext_eval ((p *' LMq),x))) by A0, Th19

          .= ((( Ext_eval (p,x)) * ( Ext_eval (r,x))) + ( Ext_eval ((p *' LMq),x))) by A2, A3, A5

          .= ((( Ext_eval (p,x)) * ( Ext_eval (r,x))) + (( Ext_eval (p,x)) * ( Ext_eval (LMq,x)))) by A0, Th22

          .= (( Ext_eval (p,x)) * (( Ext_eval (r,x)) + ( Ext_eval (LMq,x)))) by VECTSP_1:def 7

          .= (( Ext_eval (p,x)) * ( Ext_eval (q,x))) by A0, A6, Th19;

        end;

          suppose ( len q) = 0 ;

          then

           A7: q = ( 0_. A) by POLYNOM4: 5;

          

          hence ( Ext_eval ((p *' q),x)) = ( Ext_eval (( 0_. A),x)) by POLYNOM3: 34

          .= (( Ext_eval (p,x)) * ( 0. B)) by Th17

          .= (( Ext_eval (p,x)) * ( Ext_eval (q,x))) by A7, Th17;

        end;

      end;

      

       A8: for n be Nat holds P[n] from NAT_1:sch 4( A1);

      ( len q) = ( len q);

      hence thesis by A8;

    end;

    theorem :: ALGNUM_1:20

    

     Th24: for B be comRing holds for p,q be Polynomial of A holds for x be Element of B st A is Subring of B holds ( Ext_eval ((p *' q),x)) = (( Ext_eval (p,x)) * ( Ext_eval (q,x)))

    proof

      let B be comRing;

      let p,q be Polynomial of A;

      let x be Element of B;

      assume

       A0: A is Subring of B;

      defpred P[ Nat] means for p be Polynomial of A holds ( len p) = $1 implies ( Ext_eval ((p *' q),x)) = (( Ext_eval (p,x)) * ( Ext_eval (q,x)));

      

       A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]

      proof

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds for p be Polynomial of A holds ( len p) = n implies ( Ext_eval ((p *' q),x)) = (( Ext_eval (p,x)) * ( Ext_eval (q,x)));

        let p be Polynomial of A;

        assume

         A3: ( len p) = k;

        per cases ;

          suppose

           A4: ( len p) <> 0 ;

          set LMp = ( Leading-Monomial p);

          consider r be Polynomial of A such that

           A5: ( len r) < ( len p) and

           A6: p = (r + ( Leading-Monomial p)) and for n be Element of NAT st n < (( len p) - 1) holds (r . n) = (p . n) by A4, POLYNOM4: 16;

          

          thus ( Ext_eval ((p *' q),x)) = ( Ext_eval (((r *' q) + (LMp *' q)),x)) by A6, POLYNOM3: 32

          .= (( Ext_eval ((r *' q),x)) + ( Ext_eval ((LMp *' q),x))) by A0, Th19

          .= ((( Ext_eval (r,x)) * ( Ext_eval (q,x))) + ( Ext_eval ((LMp *' q),x))) by A2, A3, A5

          .= ((( Ext_eval (r,x)) * ( Ext_eval (q,x))) + (( Ext_eval (LMp,x)) * ( Ext_eval (q,x)))) by A0, Th15

          .= ((( Ext_eval (r,x)) + ( Ext_eval (LMp,x))) * ( Ext_eval (q,x))) by VECTSP_1:def 7

          .= (( Ext_eval (p,x)) * ( Ext_eval (q,x))) by A0, A6, Th19;

        end;

          suppose ( len p) = 0 ;

          then

           A7: p = ( 0_. A) by POLYNOM4: 5;

          

          hence ( Ext_eval ((p *' q),x)) = ( Ext_eval (( 0_. A),x)) by POLYNOM4: 2

          .= (( 0. B) * ( Ext_eval (q,x))) by Th17

          .= (( Ext_eval (p,x)) * ( Ext_eval (q,x))) by A7, Th17;

        end;

      end;

      

       A8: for n be Nat holds P[n] from NAT_1:sch 4( A1);

      ( len p) = ( len p);

      hence thesis by A8;

    end;

    theorem :: ALGNUM_1:21

    

     Th25: for x be Element of B, z0 be Element of A st A is Subring of B holds ( Ext_eval ( <%z0%>,x)) = ( In (z0,B))

    proof

      let x be Element of B, z0 be Element of A;

      assume

       A0: A is Subring of B;

      consider F be FinSequence of B such that

       A1: ( Ext_eval ( <%z0%>,x)) = ( Sum F) and

       A2: ( len F) = ( len <%z0%>) and

       A3: for n be Element of NAT st n in ( dom F) holds (F . n) = (( In (( <%z0%> . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      per cases by A2, ALGSEQ_1:def 5, NAT_1: 25;

        suppose

         A4: ( len F) = 0 ;

        

         A5: z0 = ( <%z0%> . 0 ) by POLYNOM5: 32

        .= (( 0_. A) . 0 ) by A4, A2, POLYNOM4: 5

        .= ( 0. A) by FUNCOP_1: 7;

        ( Ext_eval ( <%z0%>,x)) = ( Ext_eval (( 0_. A),x)) by A4, A2, POLYNOM4: 5

        .= ( 0. B) by Th17

        .= ( In (z0,B)) by A5, A0, Lm5;

        hence thesis;

      end;

        suppose

         A6: ( len F) = 1;

        

        then

         A7: (F . 1) = (( In (( <%z0%> . (1 -' 1)),B)) * (( power B) . (x,(1 -' 1)))) by A3, FINSEQ_3: 25

        .= (( In (( <%z0%> . 0 ),B)) * (( power B) . (x,(1 -' 1)))) by XREAL_1: 232

        .= (( In (( <%z0%> . 0 ),B)) * (( power B) . (x, 0 ))) by XREAL_1: 232

        .= (( In (z0,B)) * (( power B) . (x, 0 ))) by POLYNOM5: 32

        .= (( In (z0,B)) * ( 1_ B)) by GROUP_1:def 7

        .= ( In (z0,B));

        ( Ext_eval ( <%z0%>,x)) = ( Sum <*( In (z0,B))*>) by A6, A7, FINSEQ_1: 40, A1

        .= ( In (z0,B)) by RLVECT_1: 44;

        hence thesis;

      end;

    end;

    theorem :: ALGNUM_1:22

    for x be Element of B, z0,z1 be Element of A st A is Subring of B holds ( Ext_eval ( <%z0, z1%>,x)) = (( In (z0,B)) + (( In (z1,B)) * x))

    proof

      let x be Element of B, z0,z1 be Element of A;

      assume

       A0: A is Subring of B;

      consider F be FinSequence of B such that

       A1: ( Ext_eval ( <%z0, z1%>,x)) = ( Sum F) and

       A2: ( len F) = ( len <%z0, z1%>) and

       A3: for n be Element of NAT st n in ( dom F) holds (F . n) = (( In (( <%z0, z1%> . (n -' 1)),B)) * (( power B) . (x,(n -' 1)))) by Def1;

      ( len F) = 0 or ... or ( len F) = 2 by A2, POLYNOM5: 39;

      per cases ;

        suppose ( len F) = 0 ;

        then

         A4: <%z0, z1%> = ( 0_. A) by A2, POLYNOM4: 5;

        

        hence ( Ext_eval ( <%z0, z1%>,x)) = ( 0. B) by Th17

        .= ( In (( 0. A),B)) by A0, Lm5

        .= ( In ((( 0_. A) . 0 ),B)) by FUNCOP_1: 7

        .= (( In (z0,B)) + (( 0. B) * x)) by A4, POLYNOM5: 38

        .= (( In (z0,B)) + (( In (( 0. A),B)) * x)) by A0, Lm5

        .= (( In (z0,B)) + (( In ((( 0_. A) . 1),B)) * x)) by FUNCOP_1: 7

        .= (( In (z0,B)) + (( In (z1,B)) * x)) by A4, POLYNOM5: 38;

      end;

        suppose

         A5: ( len F) = 1;

        

        then (F . 1) = (( In (( <%z0, z1%> . (1 -' 1)),B)) * (( power B) . (x,(1 -' 1)))) by A3, FINSEQ_3: 25

        .= (( In (( <%z0, z1%> . 0 ),B)) * (( power B) . (x,(1 -' 1)))) by XREAL_1: 232

        .= (( In (( <%z0, z1%> . 0 ),B)) * (( power B) . (x, 0 ))) by XREAL_1: 232

        .= (( In (z0,B)) * (( power B) . (x, 0 ))) by POLYNOM5: 38

        .= (( In (z0,B)) * ( 1_ B)) by GROUP_1:def 7

        .= ( In (z0,B));

        then F = <*( In (z0,B))*> by A5, FINSEQ_1: 40;

        

        hence ( Ext_eval ( <%z0, z1%>,x)) = (( In (z0,B)) + (( 0. B) * x)) by A1, RLVECT_1: 44

        .= (( In (z0,B)) + (( In (( 0. A),B)) * x)) by A0, Lm5

        .= (( In (z0,B)) + (( In (( <%z0, z1%> . 1),B)) * x)) by A2, A5, ALGSEQ_1: 8

        .= (( In (z0,B)) + (( In (z1,B)) * x)) by POLYNOM5: 38;

      end;

        suppose

         A6: ( len F) = 2;

        

        then

         A7: (F . 1) = (( In (( <%z0, z1%> . (1 -' 1)),B)) * (( power B) . (x,(1 -' 1)))) by A3, FINSEQ_3: 25

        .= (( In (( <%z0, z1%> . 0 ),B)) * (( power B) . (x,(1 -' 1)))) by XREAL_1: 232

        .= (( In (( <%z0, z1%> . 0 ),B)) * (( power B) . (x, 0 ))) by XREAL_1: 232

        .= (( In (z0,B)) * (( power B) . (x, 0 ))) by POLYNOM5: 38

        .= (( In (z0,B)) * ( 1_ B)) by GROUP_1:def 7

        .= ( In (z0,B));

        

         A8: (2 -' 1) = (2 - 1) by XREAL_0:def 2;

        (F . 2) = (( In (( <%z0, z1%> . (2 -' 1)),B)) * (( power B) . (x,(2 -' 1)))) by A3, A6, FINSEQ_3: 25

        .= (( In (z1,B)) * (( power B) . (x,1))) by A8, POLYNOM5: 38

        .= (( In (z1,B)) * x) by GROUP_1: 50;

        then F = <*( In (z0,B)), (( In (z1,B)) * x)*> by A6, A7, FINSEQ_1: 44;

        hence thesis by A1, RLVECT_1: 45;

      end;

    end;

    begin

    definition

      let A,B be Ring;

      let x be Element of B;

      :: ALGNUM_1:def2

      pred x is_integral_over A means ex f be Polynomial of A st ( LC f) = ( 1. A) & ( Ext_eval (f,x)) = ( 0. B);

    end

    theorem :: ALGNUM_1:23

    

     Th27: for A be non degenerated Ring holds for a be Element of A st A is Subring of B holds ( In (a,B)) is_integral_over A

    proof

      let A be non degenerated Ring;

      let a be Element of A;

      assume

       A0: A is Subring of B;

      set p = <%( - a), ( 1. A)%>;

      (p . (( len p) -' 1)) = (p . (2 -' 1)) by POLYNOM5: 40

      .= (p . (2 - 1)) by XREAL_1: 233

      .= (p . 1);

      then

       A2: ( LC p) = ( 1. A) by POLYNOM5: 38;

      

       A3: ( eval (p,a)) = (( - a) + a) by POLYNOM5: 47

      .= (a - a)

      .= ( 0. A) by RLVECT_1: 15;

      ( Ext_eval (p,( In (a,B)))) = ( In (( eval (p,a)),B)) by A0, Th16

      .= ( 0. B) by A0, Lm5, A3;

      hence thesis by A2;

    end;

    definition

      let A be non degenerated Ring, B be Ring;

      assume

       A0: A is Subring of B;

      :: ALGNUM_1:def3

      func integral_closure (A,B) -> non empty Subset of B equals { z where z be Element of B : z is_integral_over A };

      coherence

      proof

        set M = { z where z be Element of B : z is_integral_over A };

         A1:

        now

          let u be object;

          assume u in M;

          then ex z be Element of B st u = z & z is_integral_over A;

          hence u in the carrier of B;

        end;

        ( In (( 0. A),B)) is_integral_over A by A0, Th27;

        then ( 0. B) is_integral_over A by A0, Lm5;

        then ( 0. B) in M;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    definition

      let c be Complex;

      :: ALGNUM_1:def4

      attr c is algebraic means ex x be Element of F_Complex st x = c & x is_integral_over F_Rat ;

    end

    definition

      let x be Element of F_Complex ;

      :: original: algebraic

      redefine

      :: ALGNUM_1:def5

      attr x is algebraic means x is_integral_over F_Rat ;

      compatibility ;

    end

    definition

      let c be Complex;

      :: ALGNUM_1:def6

      attr c is algebraic_integer means ex x be Element of F_Complex st x = c & x is_integral_over INT.Ring ;

    end

    definition

      let x be Element of F_Complex ;

      :: original: algebraic_integer

      redefine

      :: ALGNUM_1:def7

      attr x is algebraic_integer means x is_integral_over INT.Ring ;

      compatibility ;

    end

    notation

      let x be Complex;

      antonym x is transcendental for x is algebraic;

    end

    registration

      cluster rational -> algebraic for Complex;

      coherence

      proof

        let c be Complex;

        assume c is rational;

        then

        reconsider c as Element of F_Rat by RAT_1:def 2;

        take ( In (c, F_Complex ));

        thus thesis by Th3, Th27;

      end;

    end

    registration

      cluster algebraic for Complex;

      existence by GAUSSINT: 14;

      cluster algebraic for Element of F_Complex ;

      existence by Lm7;

    end

    registration

      cluster integer -> algebraic_integer for Complex;

      coherence

      proof

        let c be Complex;

        assume c is integer;

        then

        reconsider c as Element of INT.Ring by INT_1:def 2;

        take ( In (c, F_Complex ));

        thus thesis by Th4, Th27;

      end;

    end

    registration

      cluster algebraic_integer for Complex;

      existence by GAUSSINT: 14;

      cluster algebraic_integer for Element of F_Complex ;

      existence by Lm7;

    end

    definition

      let A,B be Ring;

      let x be Element of B;

      :: ALGNUM_1:def8

      func Ann_Poly (x,A) -> non empty Subset of ( Polynom-Ring A) equals { p where p be Polynomial of A : ( Ext_eval (p,x)) = ( 0. B) };

      coherence

      proof

        set M = { p where p be Polynomial of A : ( Ext_eval (p,x)) = ( 0. B) };

         A1:

        now

          let u be object;

          assume u in M;

          then ex p1 be Polynomial of A st u = p1 & ( Ext_eval (p1,x)) = ( 0. B);

          hence u in the carrier of ( Polynom-Ring A) by POLYNOM3:def 10;

        end;

        ( Ext_eval (( 0_. A),x)) = ( 0. B) by Th17;

        then ( 0_. A) in M;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: ALGNUM_1:24

    

     Lm30: for A,B be Ring, w be Element of B, x,y be Element of ( Polynom-Ring A) st A is Subring of B & x in ( Ann_Poly (w,A)) & y in ( Ann_Poly (w,A)) holds (x + y) in ( Ann_Poly (w,A))

    proof

      let A, B;

      let w be Element of B;

      let x,y be Element of ( Polynom-Ring A);

      assume that

       A0: A is Subring of B and

       A1: x in ( Ann_Poly (w,A)) and

       A2: y in ( Ann_Poly (w,A));

      reconsider x1 = x, y1 = y as Polynomial of A by POLYNOM3:def 10;

      set M = { p where p be Polynomial of A : ( Ext_eval (p,w)) = ( 0. B) };

      consider x2 be Polynomial of A such that

       A3: x2 = x1 and

       A4: ( Ext_eval (x2,w)) = ( 0. B) by A1;

      consider y2 be Polynomial of A such that

       A5: y2 = y1 and

       A6: ( Ext_eval (y2,w)) = ( 0. B) by A2;

      

       A7: ( Ext_eval ((x2 + y2),w)) = (( Ext_eval (x1,w)) + ( 0. B)) by A0, Th19, A6, A3

      .= ( 0. B) by A3, A4;

      consider t be Polynomial of A such that

       A8: t = (x1 + y1) and

       A9: ( Ext_eval (t,w)) = ( 0. B) by A3, A5, A7;

      (x1 + y1) in M by A8, A9;

      hence thesis by POLYNOM3:def 10;

    end;

    theorem :: ALGNUM_1:25

    

     Th31: for B be comRing, z be Element of B, p,x be Element of ( Polynom-Ring A) st A is Subring of B & x in ( Ann_Poly (z,A)) holds (p * x) in ( Ann_Poly (z,A))

    proof

      let B be comRing;

      let w be Element of B;

      let p,x be Element of ( Polynom-Ring A);

      assume that

       A0: A is Subring of B and

       A1: x in ( Ann_Poly (w,A));

      set M = { p where p be Polynomial of A : ( Ext_eval (p,w)) = ( 0. B) };

      reconsider p1 = p, x1 = x as Polynomial of A by POLYNOM3:def 10;

      consider x2 be Polynomial of A such that

       A2: x2 = x1 and

       A3: ( Ext_eval (x2,w)) = ( 0. B) by A1;

      ( Ext_eval ((p1 *' x1),w)) = (( Ext_eval (p1,w)) * ( 0. B)) by A0, A2, A3, Th24

      .= ( 0. B);

      then

      consider t be Polynomial of A such that

       A4: t = (p1 *' x1) and

       A5: ( Ext_eval (t,w)) = ( 0. B);

      (p1 *' x1) in M by A4, A5;

      hence thesis by POLYNOM3:def 10;

    end;

    theorem :: ALGNUM_1:26

    

     Lm32: for B be comRing holds for w be Element of B, p,x be Element of ( Polynom-Ring A) st A is Subring of B & x in ( Ann_Poly (w,A)) holds (x * p) in ( Ann_Poly (w,A))

    proof

      let B be comRing;

      let w be Element of B;

      let p,x be Element of ( Polynom-Ring A);

      set M = { p where p be Polynomial of A : ( Ext_eval (p,w)) = ( 0. B) };

      reconsider p1 = p, x1 = x as Polynomial of A by POLYNOM3:def 10;

      assume that

       A0: A is Subring of B and

       A1: x in ( Ann_Poly (w,A));

      consider x2 be Polynomial of A such that

       A2: x2 = x1 and

       A3: ( Ext_eval (x2,w)) = ( 0. B) by A1;

      ( Ext_eval ((x1 *' p1),w)) = (( Ext_eval (p1,w)) * ( 0. B)) by A0, A2, A3, Th24

      .= ( 0. B);

      then

      consider t be Polynomial of A such that

       A4: t = (x1 *' p1) and

       A5: ( Ext_eval (t,w)) = ( 0. B);

      (x1 *' p1) in M by A4, A5;

      hence thesis by POLYNOM3:def 10;

    end;

    theorem :: ALGNUM_1:27

    

     Th33: for A be non degenerated Ring holds for B be non degenerated comRing holds for w be Element of B st A is Subring of B holds ( Ann_Poly (w,A)) is proper Ideal of ( Polynom-Ring A)

    proof

      let A be non degenerated Ring;

      let B be non degenerated comRing;

      let w be Element of B;

      assume

       A0: A is Subring of B;

      

       A1: ( Ann_Poly (w,A)) is add-closed by A0, Lm30;

      

       A2: ( Ann_Poly (w,A)) is left-ideal by A0, Th31;

      

       A3: ( Ann_Poly (w,A)) is right-ideal by A0, Lm32;

      ( Ann_Poly (w,A)) is proper

      proof

        assume not ( Ann_Poly (w,A)) is proper;

        then

         A5: ( 1. ( Polynom-Ring A)) in ( Ann_Poly (w,A));

        

         A6: ( 1_. A) in ( Ann_Poly (w,A)) by A5, POLYNOM3: 37;

        

         A7: ( Ext_eval (( 1_. A),w)) = ( 1. B) by A0, Th18;

        ex p be Polynomial of A st p = ( 1_. A) & ( Ext_eval (p,w)) = ( 0. B) by A6;

        hence contradiction by A7;

      end;

      hence thesis by A1, A2, A3;

    end;

    begin

    reserve K,L for Field;

    theorem :: ALGNUM_1:28

    

     Th34: for K,L be Field, w be Element of L st K is Subring of L holds ex g be Element of ( Polynom-Ring K) st ( {g} -Ideal ) = ( Ann_Poly (w,K))

    proof

      let K, L;

      let w be Element of L;

      assume

       A0: K is Subring of L;

      

       A1: ( Polynom-Ring K) is PID;

      ( Ann_Poly (w,K)) is Ideal of ( Polynom-Ring K) by A0, Th33;

      hence thesis by A1, IDEAL_1:def 27;

    end;

    theorem :: ALGNUM_1:29

    

     Th35: for K,L be Field, z be Element of L st z is_integral_over K holds ( Ann_Poly (z,K)) <> {( 0. ( Polynom-Ring K))}

    proof

      let K, L;

      let z be Element of L;

      assume

       A1: z is_integral_over K;

      set M = { p where p be Polynomial of K : ( Ext_eval (p,z)) = ( 0. L) };

      consider f be Polynomial of K such that

       A2: ( LC f) = ( 1. K) and

       A3: ( Ext_eval (f,z)) = ( 0. L) by A1;

       not f in {( 0. ( Polynom-Ring K))}

      proof

        assume

         A5: f in {( 0. ( Polynom-Ring K))};

        reconsider f as Element of ( Polynom-Ring K) by POLYNOM3:def 10;

        f in ( {( 0. ( Polynom-Ring K))} -Ideal ) by A5, IDEAL_1: 47;

        then f in the set of all (( 0. ( Polynom-Ring K)) * g) where g be Element of ( Polynom-Ring K) by IDEAL_1: 64;

        then

        consider g1 be Element of ( Polynom-Ring K) such that

         A6: f = (( 0. ( Polynom-Ring K)) * g1);

        reconsider g2 = g1 as Polynomial of K by POLYNOM3:def 10;

        reconsider h2 = ( 0. ( Polynom-Ring K)) as Polynomial of K by POLYNOM3:def 10;

        f = ( 0_. K) by POLYNOM3:def 10, A6;

        hence contradiction by FUNCOP_1: 7, A2;

      end;

      hence thesis by A3;

    end;

    theorem :: ALGNUM_1:30

    

     Lm37: for K be Field, p be Element of ( Polynom-Ring K) st p <> ( 0_. K) holds p is non zero Element of the carrier of ( Polynom-Ring K)

    proof

      let K;

      let p be Element of ( Polynom-Ring K);

      assume

       A0: p <> ( 0_. K);

      assume

       A1: not (p is non zero Element of the carrier of ( Polynom-Ring K));

      reconsider p as Element of the carrier of ( Polynom-Ring K);

      p is zero by A1;

      hence contradiction by A0;

    end;

    theorem :: ALGNUM_1:31

    

     Th38: for K,L be Field, w be Element of L st K is Subring of L holds ( Ann_Poly (w,K)) is quasi-prime

    proof

      let K, L;

      let w be Element of L;

      assume

       A0: K is Subring of L;

      set M = { p where p be Polynomial of K : ( Ext_eval (p,w)) = ( 0. L) };

      for p,q be Element of ( Polynom-Ring K) st (p * q) in ( Ann_Poly (w,K)) holds p in ( Ann_Poly (w,K)) or q in ( Ann_Poly (w,K))

      proof

        let p,q be Element of ( Polynom-Ring K);

        assume

         A1: (p * q) in ( Ann_Poly (w,K));

        reconsider p1 = p, q1 = q as Polynomial of K by POLYNOM3:def 10;

        (p1 *' q1) in ( Ann_Poly (w,K)) by A1, POLYNOM3:def 10;

        then

        consider t be Polynomial of K such that

         A5: t = (p1 *' q1) and

         A6: ( Ext_eval (t,w)) = ( 0. L);

        (( Ext_eval (p1,w)) * ( Ext_eval (q1,w))) = ( 0. L) by A0, Th24, A6, A5;

        per cases by VECTSP_2:def 1;

          suppose ( Ext_eval (p1,w)) = ( 0. L);

          hence thesis;

        end;

          suppose ( Ext_eval (q1,w)) = ( 0. L);

          hence thesis;

        end;

      end;

      hence thesis by RING_1:def 1;

    end;

    theorem :: ALGNUM_1:32

    

     Th39: for K,L be Field, w be Element of L st K is Subring of L & w is_integral_over K holds ( Ann_Poly (w,K)) is prime

    proof

      let K, L;

      let w be Element of L;

      assume K is Subring of L & w is_integral_over K;

      then ( Ann_Poly (w,K)) is proper quasi-prime by Th38, Th33;

      hence thesis;

    end;

    theorem :: ALGNUM_1:33

    

     Th40: for K,L be Field, z be Element of L st K is Subring of L & z is_integral_over K holds ex f be Element of ( Polynom-Ring K) st f <> ( 0_. K) & ( {f} -Ideal ) = ( Ann_Poly (z,K)) & f = ( NormPolynomial f)

    proof

      let K,L be Field;

      let z be Element of L;

      assume that

       A0: K is Subring of L and

       A1: z is_integral_over K;

      consider f be Element of ( Polynom-Ring K) such that

       A2: ( {f} -Ideal ) = ( Ann_Poly (z,K)) by A0, Th34;

      

       A3: f <> ( 0. ( Polynom-Ring K)) by A1, A2, Th35, IDEAL_1: 47;

      reconsider f as Element of ( Polynom-Ring K);

      

       A4: f <> ( 0_. K) by A3, POLYNOM3:def 10;

      set g = ( NormPolynomial f);

      

       A7: ( {g} -Ideal ) = ( Ann_Poly (z,K)) by A2, RING_4: 27, RING_2: 21;

      g <> ( 0. ( Polynom-Ring K)) by A1, A7, Th35, IDEAL_1: 47;

      then

       A8: g <> ( 0_. K) by POLYNOM3:def 10;

      then

       A9: g is non zero Element of the carrier of ( Polynom-Ring K) by Lm37;

      

       A10: f is non zero Element of the carrier of ( Polynom-Ring K) by A4, Lm37;

      g = ( NormPolynomial g) by A9, A10, RING_4: 24;

      hence thesis by A7, A8;

    end;

    theorem :: ALGNUM_1:34

    

     Th41: for K,L be Field, z be Element of L, f,g be Element of ( Polynom-Ring K) st z is_integral_over K & ( {f} -Ideal ) = ( Ann_Poly (z,K)) & f = ( NormPolynomial f) & ( {g} -Ideal ) = ( Ann_Poly (z,K)) & g = ( NormPolynomial g) holds f = g

    proof

      let K,L be Field;

      let z be Element of L;

      let f,g be Element of ( Polynom-Ring K);

      assume that

       A1: z is_integral_over K and

       A2: ( {f} -Ideal ) = ( Ann_Poly (z,K)) and

       A3: f = ( NormPolynomial f) and

       A4: ( {g} -Ideal ) = ( Ann_Poly (z,K)) and

       A5: g = ( NormPolynomial g);

      reconsider f as Element of the carrier of ( Polynom-Ring K);

      ( NormPolynomial f) <> ( 0. ( Polynom-Ring K)) by A3, A2, A1, Th35, IDEAL_1: 47;

      then f <> ( 0_. K) by A3, POLYNOM3:def 10;

      then

       A6: f is non zero Element of the carrier of ( Polynom-Ring K) by Lm37;

      reconsider g as Element of the carrier of ( Polynom-Ring K);

      ( NormPolynomial g) <> ( 0. ( Polynom-Ring K)) by A5, A4, A1, Th35, IDEAL_1: 47;

      then g <> ( 0_. K) by A5, POLYNOM3:def 10;

      then g is non zero Element of the carrier of ( Polynom-Ring K) by Lm37;

      hence thesis by A3, A6, A5, RING_2: 21, RING_4: 30, A4, A2;

    end;

    definition

      let K,L be Field;

      let z be Element of L;

      assume that

       A1: K is Subring of L and

       A2: z is_integral_over K;

      :: ALGNUM_1:def9

      func minimal_polynom (z,K) -> Element of the carrier of ( Polynom-Ring K) means

      : Def7: it <> ( 0_. K) & ( {it } -Ideal ) = ( Ann_Poly (z,K)) & it = ( NormPolynomial it );

      existence by A1, A2, Th40;

      uniqueness by Th41, A2;

    end

    definition

      let K,L be Field;

      let z be Element of L;

      assume that

       A1: K is Subring of L and

       A2: z is_integral_over K;

      :: ALGNUM_1:def10

      func deg_of_integral_element (z,K) -> Element of NAT equals ( deg ( minimal_polynom (z,K)));

      coherence

      proof

        set f = ( minimal_polynom (z,K));

        

         A7: f is non zero by A1, A2, Def7;

        reconsider f as Polynomial of K;

        ( deg f) <> ( - 1) by A7;

        then

         A8: ( len f) <> 0 ;

        (( len f) + 1) > ( 0 + 1) by A8, XREAL_1: 8;

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

        hence thesis by INT_1: 3;

      end;

    end

    definition

      let A,B be Ring;

      let x be Element of B;

      :: ALGNUM_1:def11

      func hom_Ext_eval (x,A) -> Function of ( Polynom-Ring A), B means

      : Def9: for p be Polynomial of A holds (it . p) = ( Ext_eval (p,x));

      existence

      proof

        defpred P[ set, set] means ex p be Polynomial of A st p = $1 & $2 = ( Ext_eval (p,x));

        

         A1: for y be Element of the carrier of ( Polynom-Ring A) holds ex z be Element of B st P[y, z]

        proof

          let y be Element of the carrier of ( Polynom-Ring A);

          reconsider p = y as Polynomial of A;

          take ( Ext_eval (p,x));

          take p;

          thus thesis;

        end;

        consider f be Function of ( Polynom-Ring A), B such that

         A2: for y be Element of ( Polynom-Ring A) holds P[y, (f . y)] from FUNCT_2:sch 3( A1);

        reconsider f as Function of ( Polynom-Ring A), B;

        take f;

        let p be Polynomial of A;

        p in ( Polynom-Ring A) by POLYNOM3:def 10;

        then ex q be Polynomial of A st q = p & (f . p) = ( Ext_eval (q,x)) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( Polynom-Ring A), B such that

         A3: for p be Polynomial of A holds (f1 . p) = ( Ext_eval (p,x)) and

         A4: for p be Polynomial of A holds (f2 . p) = ( Ext_eval (p,x));

        now

          let y be Element of ( Polynom-Ring A);

          reconsider p = y as Polynomial of A by POLYNOM3:def 10;

          

          thus (f1 . y) = ( Ext_eval (p,x)) by A3

          .= (f2 . y) by A4;

        end;

        hence f1 = f2;

      end;

    end

    registration

      let x be Element of F_Complex ;

      cluster ( hom_Ext_eval (x, F_Rat )) -> unity-preserving additive multiplicative;

      coherence

      proof

        

        thus (( hom_Ext_eval (x, F_Rat )) . ( 1_ ( Polynom-Ring F_Rat ))) = (( hom_Ext_eval (x, F_Rat )) . ( 1_. F_Rat )) by POLYNOM3: 37

        .= ( Ext_eval (( 1_. F_Rat ),x)) by Def9

        .= ( 1_ F_Complex ) by Th3, Th18;

        hereby

          let a,b be Element of ( Polynom-Ring F_Rat );

          reconsider p = a, q = b as Polynomial of F_Rat by POLYNOM3:def 10;

          

          thus (( hom_Ext_eval (x, F_Rat )) . (a + b)) = (( hom_Ext_eval (x, F_Rat )) . (p + q)) by POLYNOM3:def 10

          .= ( Ext_eval ((p + q),x)) by Def9

          .= (( Ext_eval (p,x)) + ( Ext_eval (q,x))) by Th3, Th19

          .= ((( hom_Ext_eval (x, F_Rat )) . a) + ( Ext_eval (q,x))) by Def9

          .= ((( hom_Ext_eval (x, F_Rat )) . a) + (( hom_Ext_eval (x, F_Rat )) . b)) by Def9;

        end;

        hereby

          let a,b be Element of ( Polynom-Ring F_Rat );

          reconsider p = a, q = b as Polynomial of F_Rat by POLYNOM3:def 10;

          

          thus (( hom_Ext_eval (x, F_Rat )) . (a * b)) = (( hom_Ext_eval (x, F_Rat )) . (p *' q)) by POLYNOM3:def 10

          .= ( Ext_eval ((p *' q),x)) by Def9

          .= (( Ext_eval (p,x)) * ( Ext_eval (q,x))) by Th3, Th24

          .= ((( hom_Ext_eval (x, F_Rat )) . a) * ( Ext_eval (q,x))) by Def9

          .= ((( hom_Ext_eval (x, F_Rat )) . a) * (( hom_Ext_eval (x, F_Rat )) . b)) by Def9;

        end;

      end;

    end

    theorem :: ALGNUM_1:35

    for x be Element of F_Complex holds F_Complex is ( Polynom-Ring F_Rat ) -homomorphic

    proof

      let x be Element of F_Complex ;

      ( hom_Ext_eval (x, F_Rat )) is RingHomomorphism;

      hence thesis;

    end;

    theorem :: ALGNUM_1:36

    

     Lm45: for x be Element of B, z be object st z in ( rng ( hom_Ext_eval (x,A))) holds z in B;

    definition

      let x be Element of F_Complex ;

      :: ALGNUM_1:def12

      func FQ (x) -> Subset of F_Complex equals ( rng ( hom_Ext_eval (x, F_Rat )));

      coherence ;

    end

    registration

      let x be Element of F_Complex ;

      cluster ( FQ x) -> non empty;

      coherence ;

    end

    theorem :: ALGNUM_1:37

    

     Lm46: for x,z1,z2 be Element of F_Complex st z1 in ( FQ x) & z2 in ( FQ x) holds (z1 + z2) in ( FQ x)

    proof

      let x,z1,z2 be Element of F_Complex ;

      assume that

       A1: z1 in ( FQ x) and

       A2: z2 in ( FQ x);

      consider f1 be object such that

       A3: f1 in ( dom ( hom_Ext_eval (x, F_Rat ))) and

       A4: z1 = (( hom_Ext_eval (x, F_Rat )) . f1) by A1, FUNCT_1:def 3;

      consider f2 be object such that

       A5: f2 in ( dom ( hom_Ext_eval (x, F_Rat ))) and

       A6: z2 = (( hom_Ext_eval (x, F_Rat )) . f2) by A2, FUNCT_1:def 3;

      

       A7: ( dom ( hom_Ext_eval (x, F_Rat ))) = the carrier of ( Polynom-Ring F_Rat ) by FUNCT_2:def 1;

      reconsider g1 = f1, g2 = f2 as Polynomial of F_Rat by A3, A5, POLYNOM3:def 10;

      

       A8: (z1 + z2) = (( Ext_eval (g1,x)) + (( hom_Ext_eval (x, F_Rat )) . f2)) by Def9, A6, A4

      .= (( Ext_eval (g1,x)) + ( Ext_eval (g2,x))) by Def9

      .= ( Ext_eval ((g1 + g2),x)) by Th3, Th19

      .= (( hom_Ext_eval (x, F_Rat )) . (g1 + g2)) by Def9;

      set g = (g1 + g2);

      g in ( dom ( hom_Ext_eval (x, F_Rat ))) by A7, POLYNOM3:def 10;

      hence thesis by A8, FUNCT_1:def 3;

    end;

    theorem :: ALGNUM_1:38

    

     Lm47: for x,z1,z2 be Element of F_Complex st z1 in ( FQ x) & z2 in ( FQ x) holds (z1 * z2) in ( FQ x)

    proof

      let x,z1,z2 be Element of F_Complex ;

      assume that

       A1: z1 in ( FQ x) and

       A2: z2 in ( FQ x);

      consider f1 be object such that

       A3: f1 in ( dom ( hom_Ext_eval (x, F_Rat ))) and

       A4: z1 = (( hom_Ext_eval (x, F_Rat )) . f1) by A1, FUNCT_1:def 3;

      consider f2 be object such that

       A5: f2 in ( dom ( hom_Ext_eval (x, F_Rat ))) and

       A6: z2 = (( hom_Ext_eval (x, F_Rat )) . f2) by A2, FUNCT_1:def 3;

      

       A7: ( dom ( hom_Ext_eval (x, F_Rat ))) = the carrier of ( Polynom-Ring F_Rat ) by FUNCT_2:def 1;

      reconsider g1 = f1, g2 = f2 as Polynomial of F_Rat by A3, A5, POLYNOM3:def 10;

      

       A8: (z1 * z2) = (( Ext_eval (g1,x)) * (( hom_Ext_eval (x, F_Rat )) . f2)) by Def9, A6, A4

      .= (( Ext_eval (g1,x)) * ( Ext_eval (g2,x))) by Def9

      .= ( Ext_eval ((g1 *' g2),x)) by Th3, Th24

      .= (( hom_Ext_eval (x, F_Rat )) . (g1 *' g2)) by Def9;

      set g = (g1 *' g2);

      g in ( dom ( hom_Ext_eval (x, F_Rat ))) by A7, POLYNOM3:def 10;

      hence thesis by A8, FUNCT_1:def 3;

    end;

    theorem :: ALGNUM_1:39

    

     Lm48: for x be Element of F_Complex , a be Element of F_Rat holds a in ( FQ x)

    proof

      let x be Element of F_Complex ;

      let a be Element of F_Rat ;

      reconsider f = <%a%> as Polynomial of F_Rat ;

      

       A2: ( dom ( hom_Ext_eval (x, F_Rat ))) = the carrier of ( Polynom-Ring F_Rat ) by FUNCT_2:def 1;

      

       A3: ( Ext_eval (f,x)) = ( In (a, F_Complex )) by Th3, Th25;

      reconsider f as Element of ( Polynom-Ring F_Rat ) by POLYNOM3:def 10;

      ( In (a, F_Complex )) = (( hom_Ext_eval (x, F_Rat )) . f) by A3, Def9;

      hence thesis by A2, FUNCT_1:def 3;

    end;

    definition

      let x be Element of F_Complex ;

      :: ALGNUM_1:def13

      func FQ_add (x) -> BinOp of ( FQ x) equals ( addcomplex || ( FQ x));

      correctness

      proof

        set ad = ( addcomplex || ( FQ x));

        set theCFComplex = the carrier of F_Complex ;

        

         A0: [:( FQ x), ( FQ x):] c= [:theCFComplex, theCFComplex:];

        theCFComplex = COMPLEX by COMPLFLD:def 1;

        then [:( FQ x), ( FQ x):] c= ( dom addcomplex ) by A0, FUNCT_2:def 1;

        then

         A1: ( dom ad) = [:( FQ x), ( FQ x):] by RELAT_1: 62;

        for z be object st z in [:( FQ x), ( FQ x):] holds (ad . z) in ( FQ x)

        proof

          let z be object such that

           A2: z in [:( FQ x), ( FQ x):];

          consider a,b be object such that

           A3: a in ( FQ x) and

           A4: b in ( FQ x) and

           A5: z = [a, b] by A2, ZFMISC_1:def 2;

          reconsider x1 = a, y1 = b as Element of theCFComplex by A3, A4;

          (ad . z) = ( addcomplex . (a,b)) by A2, A5, FUNCT_1: 49

          .= (x1 + y1) by BINOP_2:def 3;

          hence (ad . z) in ( FQ x) by A3, A4, Lm46;

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    definition

      let x be Element of F_Complex ;

      :: ALGNUM_1:def14

      func FQ_mult (x) -> BinOp of ( FQ x) equals ( multcomplex || ( FQ x));

      correctness

      proof

        set mult = ( multcomplex || ( FQ x));

        set theCFComplex = the carrier of F_Complex ;

        

         A0: theCFComplex = COMPLEX by COMPLFLD:def 1;

         [:( FQ x), ( FQ x):] c= [: COMPLEX , COMPLEX :] by A0;

        then [:( FQ x), ( FQ x):] c= ( dom multcomplex ) by FUNCT_2:def 1;

        then

         A1: ( dom mult) = [:( FQ x), ( FQ x):] by RELAT_1: 62;

        for z be object st z in [:( FQ x), ( FQ x):] holds (mult . z) in ( FQ x)

        proof

          let z be object such that

           A2: z in [:( FQ x), ( FQ x):];

          consider x1,y1 be object such that

           A3: x1 in ( FQ x) & y1 in ( FQ x) & z = [x1, y1] by A2, ZFMISC_1:def 2;

          reconsider x2 = x1, y2 = y1 as Element of theCFComplex by A3;

          (mult . z) = ( multcomplex . (x2,y2)) by A2, A3, FUNCT_1: 49

          .= (x2 * y2) by BINOP_2:def 5;

          hence (mult . z) in ( FQ x) by A3, Lm47;

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    theorem :: ALGNUM_1:40

    

     Th49: for x be Element of F_Complex , z,w be Element of ( FQ x) holds (( FQ_add x) . (z,w)) = (z + w)

    proof

      let x be Element of F_Complex ;

      let z,w be Element of ( FQ x);

      

      thus (( FQ_add x) . (z,w)) = ( addcomplex . (z,w)) by FUNCT_1: 49, ZFMISC_1: 87

      .= (z + w) by BINOP_2:def 3;

    end;

    theorem :: ALGNUM_1:41

    

     Th50: for x be Element of F_Complex , z,w be Element of ( FQ x) holds (( FQ_mult x) . (z,w)) = (z * w)

    proof

      let x be Element of F_Complex ;

      let z,w be Element of ( FQ x);

      

      thus (( FQ_mult x) . (z,w)) = ( multcomplex . (z,w)) by FUNCT_1: 49, ZFMISC_1: 87

      .= (z * w) by BINOP_2:def 5;

    end;

    theorem :: ALGNUM_1:42

    

     Lm52: for x be Element of F_Complex holds ( In (( 1. F_Complex ),( FQ x))) = ( 1. F_Complex )

    proof

      let x be Element of F_Complex ;

      ( 1. F_Complex ) = ( 1. F_Rat ) by C0SP1:def 3, Th3;

      hence thesis by Lm48, SUBSET_1:def 8;

    end;

    theorem :: ALGNUM_1:43

    

     Lm53: ( In (( - ( 1. F_Rat )), F_Complex )) = ( - ( 1. F_Complex ))

    proof

      (( 1. F_Complex ) + ( In (( - ( 1. F_Rat )), F_Complex ))) = (( In (( 1. F_Rat ), F_Complex )) + ( In (( - ( 1. F_Rat )), F_Complex ))) by Lm5, Th3

      .= ( In (( 0. F_Rat ), F_Complex ))

      .= ( 0. F_Complex ) by Lm5, Th3;

      hence thesis by RLVECT_1:def 10;

    end;

    definition

      let x be Element of F_Complex ;

      :: ALGNUM_1:def15

      func FQ_Ring (x) -> strict non empty doubleLoopStr equals doubleLoopStr (# ( FQ x), ( FQ_add x), ( FQ_mult x), ( In (( 1. F_Complex ),( FQ x))), ( In (( 0. F_Complex ),( FQ x))) #);

      coherence ;

    end

    theorem :: ALGNUM_1:44

    

     Th54: for x be Element of F_Complex holds ( FQ_Ring x) is Ring

    proof

      let x be Element of F_Complex ;

      reconsider ZS = doubleLoopStr (# ( FQ x), ( FQ_add x), ( FQ_mult x), ( In (( 1. F_Complex ),( FQ x))), ( In (( 0. F_Complex ),( FQ x))) #) as non empty doubleLoopStr;

      

       A1: for v,w be Element of ZS holds (v + w) = (w + v)

      proof

        let v,w be Element of ZS;

        v in F_Complex & w in F_Complex by Lm45;

        then

        reconsider v1 = v, w1 = w as Element of F_Complex ;

        

        thus (v + w) = (w1 + v1) by Th49

        .= (w + v) by Th49;

      end;

      

       A2: for u,v,w be Element of ZS holds ((u + v) + w) = (u + (v + w))

      proof

        let u,v,w be Element of ZS;

        u in F_Complex & v in F_Complex & w in F_Complex by Lm45;

        then

        reconsider u1 = u, v1 = v, w1 = w as Element of F_Complex ;

        

         A3: (u + v) = (u1 + v1) by Th49;

        

         A4: (v + w) = (v1 + w1) by Th49;

        

        thus ((u + v) + w) = ((u1 + v1) + w1) by Th49, A3

        .= (u1 + (v1 + w1))

        .= (u + (v + w)) by Th49, A4;

      end;

      

       A5: for v be Element of ZS holds (v + ( 0. ZS)) = v

      proof

        let v be Element of ZS;

        

         A6: ( 0. ZS) = ( 0. F_Complex ) by Lm48, Lm7, SUBSET_1:def 8;

        ( 0. ZS) in F_Complex & v in F_Complex by Lm45;

        then

        reconsider v1 = v as Element of F_Complex ;

        

        thus (v + ( 0. ZS)) = (v1 + ( 0. F_Complex )) by Th49, A6

        .= v;

      end;

      

       A7: for v be Element of ZS holds v is right_complementable

      proof

        let v be Element of ZS;

        v in F_Complex by Lm45;

        then

        reconsider v1 = v as Element of F_Complex ;

        

         A8: (( - ( 1. F_Complex )) * v1) = ( - (( 1. F_Complex ) * v1)) by VECTSP_1: 9

        .= ( - v1);

        reconsider w1 = ( - ( 1. F_Complex )) as Element of ZS by Lm48, Lm53;

        

         A10: (w1 * v) = (( - ( 1. F_Complex )) * v1) by Th50;

        take (w1 * v);

        

        thus (v + (w1 * v)) = (v1 + (( - ( 1. F_Complex )) * v1)) by A10, Th49

        .= ( 0. F_Complex ) by RLVECT_1: 5, A8

        .= ( 0. ZS) by Lm48, Lm7, SUBSET_1:def 8;

      end;

      

       A11: for a,b,v be Element of ZS holds ((a + b) * v) = ((a * v) + (b * v))

      proof

        let a,b,v be Element of ZS;

        a in F_Complex & b in F_Complex & v in F_Complex by Lm45;

        then

        reconsider a1 = a, b1 = b, v1 = v as Element of F_Complex ;

        

         A12: (a + b) in ( FQ x);

        reconsider ab = (a + b) as Element of F_Complex by A12;

        

         A13: (a1 * v1) = (a * v) & ((b1 * v1) = (b * v)) by Th50;

        

        thus ((a + b) * v) = (ab * v1) by Th50

        .= ((a1 + b1) * v1) by Th49

        .= ((a1 * v1) + (b1 * v1))

        .= ((a * v) + (b * v)) by A13, Th49;

      end;

      

       A14: for a,v,w be Element of ZS holds (a * (v + w)) = ((a * v) + (a * w)) & ((v + w) * a) = ((v * a) + (w * a))

      proof

        let a,v,w be Element of ZS;

        a in F_Complex & v in F_Complex & w in F_Complex by Lm45;

        then

        reconsider a1 = a, v1 = v, w1 = w as Element of F_Complex ;

        

         A15: (v + w) in ( FQ x);

        reconsider vw = (v + w) as Element of F_Complex by A15;

        

         A16: ((a1 * v1) = (a * v)) & ((a1 * w1) = (a * w)) by Th50;

        

        thus (a * (v + w)) = (a1 * vw) by Th50

        .= (a1 * (v1 + w1)) by Th49

        .= ((a1 * v1) + (a1 * w1))

        .= ((a * v) + (a * w)) by A16, Th49;

        thus ((v + w) * a) = ((v * a) + (w * a)) by A11;

      end;

      

       A17: for a,b,v be Element of ZS holds ((a * b) * v) = (a * (b * v))

      proof

        let a,b,v be Element of ZS;

        a in F_Complex & b in F_Complex & v in F_Complex by Lm45;

        then

        reconsider a1 = a, b1 = b, v1 = v as Element of F_Complex ;

        

         A18: (a * b) in ( FQ x) & (b * v) in ( FQ x);

        reconsider ab = (a * b), bv = (b * v) as Element of F_Complex by A18;

        

        thus ((a * b) * v) = (ab * v1) by Th50

        .= ((a1 * b1) * v1) by Th50

        .= (a1 * (b1 * v1))

        .= (a1 * bv) by Th50

        .= (a * (b * v)) by Th50;

      end;

      for v be Element of ZS holds (v * ( 1. ZS)) = v & (( 1. ZS) * v) = v

      proof

        let v be Element of ZS;

        

         A19: ( 1. ZS) = ( 1. F_Complex ) by Lm52;

        v in F_Complex by Lm45;

        then

        reconsider v1 = v as Element of F_Complex ;

        

        thus (v * ( 1. ZS)) = (v1 * ( 1. F_Complex )) by A19, Th50

        .= v;

        

        thus (( 1. ZS) * v) = (( 1. F_Complex ) * v1) by A19, Th50

        .= v;

      end;

      hence thesis by A1, A2, A5, A7, A14, A17, VECTSP_1:def 6, VECTSP_1:def 7, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, ALGSTR_0:def 16;

    end;

    registration

      let x be Element of F_Complex ;

      cluster ( FQ_Ring x) -> Abelian add-associative right_zeroed right_complementable associative well-unital distributive;

      coherence by Th54;

    end

    registration

      let z be Element of F_Complex ;

      cluster ( FQ_Ring z) -> domRing-like commutative non degenerated;

      coherence

      proof

        set X = ( FQ_Ring z);

        thus X is domRing-like

        proof

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

          proof

            let x,y be Element of X;

            x in F_Complex & y in F_Complex by Lm45;

            then

            reconsider x1 = x, y1 = y as Element of F_Complex ;

            assume

             A1: (x * y) = ( 0. X);

            

             A2: ( 0. X) = ( 0. F_Complex ) by Lm48, Lm7, SUBSET_1:def 8;

            then (x1 * y1) = ( 0. F_Complex ) by A1, Th50;

            hence thesis by A2, VECTSP_1: 12;

          end;

          hence thesis by VECTSP_2:def 1;

        end;

        

         A3: ( 0. ( FQ_Ring z)) = ( 0. F_Complex ) by Lm48, Lm7, SUBSET_1:def 8;

        thus X is commutative

        proof

          let v,w be Element of ( FQ_Ring z);

          v in F_Complex & w in F_Complex by Lm45;

          then

          reconsider v1 = v, w1 = w as Element of F_Complex ;

          

          thus (v * w) = (v1 * w1) by Th50

          .= (w * v) by Th50;

        end;

        thus thesis by Lm52, A3;

      end;

    end

    

     Lm55: for x be Element of F_Complex holds the carrier of F_Rat c= the carrier of ( FQ_Ring x) by Lm48;

    theorem :: ALGNUM_1:45

    

     Lm56: for x be Element of F_Complex holds [: RAT , RAT :] c= [:( FQ x), ( FQ x):] & [:( FQ x), ( FQ x):] c= [: COMPLEX , COMPLEX :]

    proof

      let x be Element of F_Complex ;

      

       A1: the carrier of F_Rat c= the carrier of ( FQ_Ring x) by Lm48;

      

       A2: ( FQ x) c= the carrier of F_Complex ;

      ( FQ x) c= COMPLEX by A2, COMPLFLD:def 1;

      hence thesis by A1, ZFMISC_1: 96;

    end;

    theorem :: ALGNUM_1:46

    

     Lm57: for x be Element of F_Complex holds the addF of F_Rat = (the addF of ( FQ_Ring x) || RAT )

    proof

      let x be Element of F_Complex ;

      

      thus the addF of F_Rat = ( addcomplex | [: RAT , RAT :]) by ZFMISC_1: 96, RELAT_1: 74, VECTSP_1:def 5, RING_3: 2, GAUSSINT: 13

      .= (the addF of ( FQ_Ring x) || RAT ) by Lm56, RELAT_1: 74;

    end;

    theorem :: ALGNUM_1:47

    

     Lm58: for x be Element of F_Complex holds the multF of F_Rat = (the multF of ( FQ_Ring x) || RAT )

    proof

      let x be Element of F_Complex ;

      

      thus the multF of F_Rat = ( multcomplex | [: RAT , RAT :]) by ZFMISC_1: 96, RELAT_1: 74, VECTSP_1:def 5, RING_3: 3, GAUSSINT: 13

      .= (the multF of ( FQ_Ring x) || RAT ) by Lm56, RELAT_1: 74;

    end;

    theorem :: ALGNUM_1:48

    for x be Element of F_Complex holds F_Rat is Subring of ( FQ_Ring x)

    proof

      let x be Element of F_Complex ;

      

       A1: the addF of F_Rat = (the addF of ( FQ_Ring x) || the carrier of F_Rat ) by Lm57;

      

       A2: the multF of F_Rat = (the multF of ( FQ_Ring x) || the carrier of F_Rat ) by Lm58;

      

       A3: ( 1. ( FQ_Ring x)) = ( 1. F_Complex ) by Lm52

      .= ( 1. F_Rat ) by C0SP1:def 3, Th3;

      ( 0. ( FQ_Ring x)) = ( 0. F_Rat ) by Lm48, Lm7, SUBSET_1:def 8;

      hence thesis by Lm55, A1, A2, A3, C0SP1:def 3;

    end;

    theorem :: ALGNUM_1:49

    

     Th80: for f,g be Element of ( Polynom-Ring K) st f <> ( 0. ( Polynom-Ring K)) & ( {f} -Ideal ) is prime & not (g in ( {f} -Ideal )) holds ( {f, g} -Ideal ) = the carrier of ( Polynom-Ring K)

    proof

      let f,g be Element of ( Polynom-Ring K);

      assume that

       A1: f <> ( 0. ( Polynom-Ring K)) and

       A2: ( {f} -Ideal ) is prime and

       A4: not g in ( {f} -Ideal );

      assume

       A5: ( {f, g} -Ideal ) <> the carrier of ( Polynom-Ring K);

      ( Polynom-Ring K) is PID;

      then

      consider h be Element of ( Polynom-Ring K) such that

       A7: ( {f, g} -Ideal ) = ( {h} -Ideal ) by IDEAL_1:def 27;

      

       A8: ( {f} -Ideal ) c= ( {h} -Ideal ) & ( {g} -Ideal ) c= ( {h} -Ideal ) by A7, IDEAL_1: 69;

      consider s be Element of ( Polynom-Ring K) such that

       A9: f = (h * s) by RING_2: 19, A8, GCD_1:def 1;

      consider t be Element of ( Polynom-Ring K) such that

       A11: g = (h * t) by RING_2: 19, A8, GCD_1:def 1;

      f is non zero Element of ( Polynom-Ring K) by A1, STRUCT_0:def 12;

      then

       A13: f is prime by A2, RING_2: 24;

      per cases by A9, A13;

        suppose f divides s;

        then

        consider u be Element of ( Polynom-Ring K) such that

         A16: s = (f * u) by GCD_1:def 1;

        

         A17: f = (f * (u * h)) by GROUP_1:def 3, A9, A16;

        reconsider v = (u * h) as Element of ( Polynom-Ring K);

        ((f * ( 1. ( Polynom-Ring K))) - (f * v)) = ( 0. ( Polynom-Ring K)) by RLVECT_1: 5, A17;

        then (f * (( 1. ( Polynom-Ring K)) - v)) = ( 0. ( Polynom-Ring K)) by VECTSP_1: 11;

        then (( 1. ( Polynom-Ring K)) + ( - v)) = ( 0. ( Polynom-Ring K)) by A1, VECTSP_2:def 1;

        then h divides ( 1. ( Polynom-Ring K)) by VECTSP_1: 19, GCD_1:def 1;

        then

         A27: h is Unit of ( Polynom-Ring K) by GCD_1:def 2;

        ( [#] ( Polynom-Ring K)) = the carrier of ( Polynom-Ring K);

        hence contradiction by A5, A7, A27, RING_2: 20;

      end;

        suppose f divides h;

        then

        consider v be Element of ( Polynom-Ring K) such that

         A31: h = (f * v) by GCD_1:def 1;

        g = (f * (v * t)) by A11, A31, GROUP_1:def 3;

        hence contradiction by A4, GCD_1:def 1, RING_2: 18;

      end;

    end;

    theorem :: ALGNUM_1:50

    

     Th81: for f,g be Element of ( Polynom-Ring K) holds f <> ( 0. ( Polynom-Ring K)) & ( {f} -Ideal ) is prime & not g in ( {f} -Ideal ) implies (( {f} -Ideal ),( {g} -Ideal )) are_co-prime

    proof

      let f,g be Element of ( Polynom-Ring K);

      ( {f, g} -Ideal ) = (( {f} -Ideal ) + ( {g} -Ideal )) by IDEAL_1: 76;

      hence thesis by Th80;

    end;

    theorem :: ALGNUM_1:51

    

     Lm62: for x be Element of F_Complex , a be Element of ( FQ_Ring x) holds ex g be Element of ( Polynom-Ring F_Rat ) st a = (( hom_Ext_eval (x, F_Rat )) . g)

    proof

      let x be Element of F_Complex ;

      let a be Element of ( FQ_Ring x);

      ex g1 be object st g1 in ( dom ( hom_Ext_eval (x, F_Rat ))) & a = (( hom_Ext_eval (x, F_Rat )) . g1) by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: ALGNUM_1:52

    

     Th83: for x,a be Element of F_Complex st a <> ( 0. F_Complex ) & a in the carrier of ( FQ_Ring x) holds ex g be Element of ( Polynom-Ring F_Rat ) st not g in ( Ann_Poly (x, F_Rat )) & a = (( hom_Ext_eval (x, F_Rat )) . g)

    proof

      let x,a be Element of F_Complex ;

      set M = { p where p be Polynomial of F_Rat : ( Ext_eval (p,x)) = ( 0. F_Complex ) };

      assume that

       A1: a <> ( 0. F_Complex ) and

       A2: a in the carrier of ( FQ_Ring x);

      consider g be Element of ( Polynom-Ring F_Rat ) such that

       A3: a = (( hom_Ext_eval (x, F_Rat )) . g) by A2, Lm62;

      take g;

      thus not g in ( Ann_Poly (x, F_Rat ))

      proof

        assume g in ( Ann_Poly (x, F_Rat ));

        then

        consider g1 be Polynomial of F_Rat such that

         A5: g1 = g and

         A6: ( Ext_eval (g1,x)) = ( 0. F_Complex );

        thus contradiction by A1, A6, A3, A5, Def9;

      end;

      thus thesis by A3;

    end;

    theorem :: ALGNUM_1:53

    

     Th84: for x,a be Element of F_Complex st x is algebraic & a <> ( 0. F_Complex ) & a in the carrier of ( FQ_Ring x) holds ex f,g be Element of ( Polynom-Ring F_Rat ) st ( {f} -Ideal ) = ( Ann_Poly (x, F_Rat )) & not (g in ( Ann_Poly (x, F_Rat ))) & a = (( hom_Ext_eval (x, F_Rat )) . g) & (( {f} -Ideal ),( {g} -Ideal )) are_co-prime

    proof

      let x,a be Element of F_Complex ;

      assume that

       A1: x is algebraic and

       A2: a <> ( 0. F_Complex ) and

       A3: a in the carrier of ( FQ_Ring x);

      consider f be Element of ( Polynom-Ring F_Rat ) such that

       A4: ( {f} -Ideal ) = ( Ann_Poly (x, F_Rat )) by Th34, Th3;

      consider g be Element of ( Polynom-Ring F_Rat ) such that

       A5: not (g in ( Ann_Poly (x, F_Rat ))) and

       A6: a = (( hom_Ext_eval (x, F_Rat )) . g) by Th83, A2, A3;

      

       A7: ( {f} -Ideal ) is prime by A4, A1, Th3, Th39;

      

       A8: f <> ( 0. ( Polynom-Ring F_Rat )) by A1, A4, Th35, IDEAL_1: 47;

      (( {f} -Ideal ),( {g} -Ideal )) are_co-prime by A4, A5, A7, A8, Th81;

      hence thesis by A4, A5, A6;

    end;

    theorem :: ALGNUM_1:54

    

     Th85: for x,a be Element of F_Complex st x is algebraic & a <> ( 0. F_Complex ) & a in the carrier of ( FQ_Ring x) holds ex b be Element of F_Complex st b in the carrier of ( FQ_Ring x) & (a * b) = ( 1. F_Complex )

    proof

      let x,a be Element of F_Complex ;

      set COPolynomFRat = the carrier of ( Polynom-Ring F_Rat );

      set M = { h where h be Polynomial of F_Rat : ( Ext_eval (h,x)) = ( 0. F_Complex ) };

      assume that

       A1: x is algebraic and

       A2: a <> ( 0. F_Complex ) and

       A3: a in the carrier of ( FQ_Ring x);

      consider f,g be Element of ( Polynom-Ring F_Rat ) such that

       A4: ( {f} -Ideal ) = ( Ann_Poly (x, F_Rat )) and not (g in ( Ann_Poly (x, F_Rat ))) and

       A6: a = (( hom_Ext_eval (x, F_Rat )) . g) and

       A7: (( {f} -Ideal ),( {g} -Ideal )) are_co-prime by A1, A2, A3, Th84;

      ( 1. ( Polynom-Ring F_Rat )) in (( {f} -Ideal ) + ( {g} -Ideal )) by A7;

      then ( 1. ( Polynom-Ring F_Rat )) in { (p + q) where p,q be Element of ( Polynom-Ring F_Rat ) : p in ( {f} -Ideal ) & q in ( {g} -Ideal ) } by IDEAL_1:def 19;

      then

      consider p,q be Element of ( Polynom-Ring F_Rat ) such that

       A10: ( 1. ( Polynom-Ring F_Rat )) = (p + q) and

       A11: p in ( {f} -Ideal ) and

       A12: q in ( {g} -Ideal );

      

       A14: ( {g} -Ideal ) = the set of all (g * s) where s be Element of ( Polynom-Ring F_Rat ) by IDEAL_1: 64;

      consider s be Element of ( Polynom-Ring F_Rat ) such that

       A15: q = (g * s) by A12, A14;

      reconsider p1 = p, q1 = q, g1 = g, s1 = s as Polynomial of F_Rat by POLYNOM3:def 10;

      

       A16: (p + q) = (p1 + q1) by POLYNOM3:def 10;

      consider p2 be Polynomial of F_Rat such that

       A17: p2 = p and

       A18: ( Ext_eval (p2,x)) = ( 0. F_Complex ) by A4, A11;

      set b = ( Ext_eval (s1,x));

      

       A20: b = (( hom_Ext_eval (x, F_Rat )) . s1) by Def9;

      

       A21: ( dom ( hom_Ext_eval (x, F_Rat ))) = the carrier of ( Polynom-Ring F_Rat ) by FUNCT_2:def 1;

      

       A22: b in the carrier of ( FQ_Ring x) by A20, A21, FUNCT_1:def 3;

      ( 1. F_Complex ) = ( Ext_eval (( 1_. F_Rat ),x)) by Th3, Th18

      .= ( Ext_eval ((p1 + q1),x)) by A10, POLYNOM3:def 10, A16

      .= (( 0. F_Complex ) + ( Ext_eval (q1,x))) by A17, A18, Th3, Th19

      .= ( Ext_eval ((g1 *' s1),x)) by A15, POLYNOM3:def 10

      .= (( Ext_eval (g1,x)) * ( Ext_eval (s1,x))) by Th3, Th24

      .= (a * b) by A6, Def9;

      hence thesis by A22;

    end;

    theorem :: ALGNUM_1:55

    for x be Element of F_Complex st x is algebraic holds ( FQ_Ring x) is Field

    proof

      let x be Element of F_Complex ;

      assume

       A1: x is algebraic;

      for a be Element of ( FQ_Ring x) st a <> ( 0. ( FQ_Ring x)) holds a is left_invertible

      proof

        let a be Element of ( FQ_Ring x);

        assume a <> ( 0. ( FQ_Ring x));

        then

         A4: a <> ( 0. F_Complex ) by SUBSET_1:def 8;

        a in ( FQ x);

        then

        reconsider y = a as Element of F_Complex ;

        consider b be Element of F_Complex such that

         A5: b in the carrier of ( FQ_Ring x) and

         A6: (y * b) = ( 1. F_Complex ) by A1, A4, Th85;

        reconsider a1 = y, b1 = b as Element of ( FQ_Ring x) by A5;

        (b1 * a1) = ( 1. F_Complex ) by A6, Th50

        .= ( 1. ( FQ_Ring x)) by Lm52;

        hence thesis;

      end;

      then ( FQ_Ring x) is almost_left_invertible;

      hence ( FQ_Ring x) is Field;

    end;