hurwitz.miz

begin



 Lm1: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for F be FinSequence of L holds for G be FinSequence holds for k be Nat st G = (F | ( Seg k)) & ( len F) = (k + 1) holds G is FinSequence of L & ( dom G) c= ( dom F) & ( len G) = k & F = (G ^ <*(F /. (k + 1))*>)

 proof

 let L be add-associative right_zeroed right_complementable non empty addLoopStr;

 let F be FinSequence of L;

 let G1 be FinSequence;

 let k be Nat;

 assume that

 A1: G1 = (F | ( Seg k)) and

 A2: ( len F) = (k + 1);

 reconsider G = G1 as FinSequence;



 A3: k <= ( len F) by A2, NAT_1: 13;

 then

 A4: ( len G) = k by A1, FINSEQ_1: 17;

 now

 let u be object;

 assume u in ( rng G);

 then

 consider x be object such that

 A5: x in ( dom G) and

 A6: (G . x) = u by FUNCT_1:def 3;

 reconsider x9 = x as Element of NAT by A5;

 x9 <= ( len G) by A5, FINSEQ_3: 25;

 then

 A7: x9 <= ( len F) by A2, A4, NAT_1: 12;

 1 <= x9 by A5, FINSEQ_3: 25;

 then

 A8: x in ( dom F) by A7, FINSEQ_3: 25;

 (G . x) = (F . x) by A1, A5, FUNCT_1: 47

 .= (F /. x) by A8, PARTFUN1:def 6;

 hence u in the carrier of L by A6;

 end;

 then

 A9: ( rng G) c= the carrier of L by TARSKI:def 3;

 hence G1 is FinSequence of L by FINSEQ_1:def 4;

 reconsider G as FinSequence of L by A9, FINSEQ_1:def 4;



 A10: ( dom (G ^ <*(F /. (k + 1))*>)) = ( Seg (( len G) + ( len <*(F /. (k + 1))*>))) by FINSEQ_1:def 7

 .= ( Seg (k + 1)) by A4, FINSEQ_1: 40

 .= ( dom F) by A2, FINSEQ_1:def 3;

 hence ( dom G1) c= ( dom F) by FINSEQ_1: 26;

 thus ( len G1) = k by A1, A3, FINSEQ_1: 17;

 now

 let j be Nat;

 assume

 A11: j in ( dom F);

 per cases ;

 suppose

 A12: j in ( dom G);



 hence (F . j) = (G . j) by A1, FUNCT_1: 47

 .= ((G ^ <*(F /. (k + 1))*>) . j) by A12, FINSEQ_1:def 7;

 end;

 suppose

 A13: not j in ( dom G);



 A14: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

 then

 A15: 1 <= j by A11, FINSEQ_1: 1;

 A16:

 now

 assume j < (k + 1);

 then j <= k by NAT_1: 13;

 then j in ( Seg k) by A15;

 hence contradiction by A1, A3, A13, FINSEQ_1: 17;

 end;

 j <= (k + 1) by A2, A11, A14, FINSEQ_1: 1;

 then

 A17: j = (k + 1) by A16, XXREAL_0: 1;

 ( dom <*(F /. (k + 1))*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

 then 1 in ( dom <*(F /. (k + 1))*>) by TARSKI:def 1;



 hence ((G ^ <*(F /. (k + 1))*>) . j) = ( <*(F /. (k + 1))*> . 1) by A4, A17, FINSEQ_1:def 7

 .= (F /. (k + 1)) by FINSEQ_1: 40

 .= (F . j) by A11, A17, PARTFUN1:def 6;

 end;

 end;

 hence thesis by A10, FINSEQ_1: 13;

 end;

 theorem :: HURWITZ:1



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

 proof

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

 let x be Element of L;

 assume

 A1: x <> ( 0. L);

 A2:

 now

 assume ( - x) = ( 0. L);

 then ( - ( - x)) = ( 0. L) by RLVECT_1: 12;

 hence contradiction by A1, RLVECT_1: 17;

 end;

 (( - x) * ( - (x " ))) = ( - (( - x) * (x " ))) by VECTSP_1: 8

 .= ( - ( - (x * (x " )))) by VECTSP_1: 8

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

 .= ( 1_ L) by RLVECT_1: 17;

 hence thesis by A2, VECTSP_1:def 10;

 end;

 theorem :: HURWITZ:2



 Th2: for L be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non degenerated non empty doubleLoopStr holds for k be Element of NAT holds (( power L) . (( - ( 1_ L)),k)) <> ( 0. L)

 proof

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

 defpred P[ Nat] means (( power L) . (( - ( 1_ L)),$1)) <> ( 0. L);

 A1:

 now

 A2:

 now

 assume

 A3: ( - ( 1_ L)) = ( 0. L);

 ( 1_ L) = (( 1_ L) * ( 1_ L))

 .= (( - ( 1_ L)) * ( - ( 1_ L))) by VECTSP_1: 10

 .= ( 0. L) by A3;

 hence contradiction;

 end;

 let k be Nat;

 reconsider kk = k as Element of NAT by ORDINAL1:def 12;



 A4: (( power L) . (( - ( 1_ L)),(kk + 1))) = ((( power L) . (( - ( 1_ L)),kk)) * ( - ( 1_ L))) by GROUP_1:def 7;

 assume P[k];

 hence P[(k + 1)] by A4, A2, VECTSP_1: 12;

 end;



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

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

 hence thesis;

 end;

 theorem :: HURWITZ:3



 Th3: for L be associative well-unital non empty multLoopStr holds for x be Element of L holds for k1,k2 be Element of NAT holds ((( power L) . (x,k1)) * (( power L) . (x,k2))) = (( power L) . (x,(k1 + k2)))

 proof

 let L be associative well-unital non empty multLoopStr, x be Element of L, k1,k2 be Element of NAT ;

 defpred P[ Nat] means ex j be Element of NAT st j = $1 & ((( power L) . (x,k1)) * (( power L) . (x,j))) = (( power L) . (x,(k1 + j)));

 A1:

 now

 let j be Nat;

 reconsider jj = j as Element of NAT by ORDINAL1:def 12;

 assume

 A2: P[j];

 ((( power L) . (x,k1)) * (( power L) . (x,(j + 1)))) = ((( power L) . (x,k1)) * ((( power L) . (x,jj)) * x)) by GROUP_1:def 7

 .= (((( power L) . (x,k1)) * (( power L) . (x,jj))) * x) by GROUP_1:def 3

 .= (( power L) . (x,((k1 + j) + 1))) by A2, GROUP_1:def 7

 .= (( power L) . (x,(k1 + (j + 1))));

 hence P[(j + 1)];

 end;

 ( 1_ L) = ( 1. L);



 then ((( power L) . (x,k1)) * (( power L) . (x, 0 ))) = ((( power L) . (x,k1)) * ( 1. L)) by GROUP_1:def 7

 .= (( power L) . (x,(k1 + 0 )));

 then

 A3: P[ 0 ];

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

 then ex j be Element of NAT st j = k2 & ((( power L) . (x,k1)) * (( power L) . (x,j))) = (( power L) . (x,(k1 + j)));

 hence thesis;

 end;



 Lm2: ( Im ( 1_ F_Complex )) = 0 & ( Im ( - ( 1_ F_Complex ))) = 0 & ( Im ( 0. F_Complex )) = 0

 proof

 thus ( Im ( 1_ F_Complex )) = 0 by COMPLEX1: 6, COMPLFLD: 8;

 ( - ( 1_ F_Complex )) = ( - 1r ) by COMPLFLD: 2, COMPLFLD: 8;



 hence ( Im ( - ( 1_ F_Complex ))) = ( - 0 ) by COMPLEX1: 6, COMPLEX1: 17

 .= 0 ;

 thus thesis by COMPLEX1: 4, COMPLFLD: 7;

 end;

 theorem :: HURWITZ:4



 Th4: for L be add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr holds for k be Element of NAT holds (( power L) . (( - ( 1_ L)),(2 * k))) = ( 1_ L) & (( power L) . (( - ( 1_ L)),((2 * k) + 1))) = ( - ( 1_ L))

 proof

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

 defpred P[ Nat] means (( power L) . (( - ( 1_ L)),(2 * $1))) = ( 1_ L) & (( power L) . (( - ( 1_ L)),((2 * $1) + 1))) = ( - ( 1_ L));

 A1:

 now

 let k be Nat;

 assume

 A2: P[k];



 A3: (( power L) . (( - ( 1_ L)),(2 * (k + 1)))) = (( power L) . (( - ( 1_ L)),(((2 * k) + 1) + 1)))

 .= ((( power L) . (( - ( 1_ L)),((2 * k) + 1))) * ( - ( 1_ L))) by GROUP_1:def 7

 .= ( - (( 1_ L) * ( - ( 1_ L)))) by A2, VECTSP_1: 9

 .= ( - ( - ( 1_ L)))

 .= ( 1_ L) by RLVECT_1: 17;

 (( power L) . (( - ( 1_ L)),((2 * (k + 1)) + 1))) = ((( power L) . (( - ( 1_ L)),(2 * (k + 1)))) * ( - ( 1_ L))) by GROUP_1:def 7

 .= ( - ( 1_ L)) by A3;

 hence P[(k + 1)] by A3;

 end;

 (( power L) . (( - ( 1_ L)),((2 * 0 ) + 1))) = ((( power L) . (( - ( 1_ L)), 0 )) * ( - ( 1_ L))) by GROUP_1:def 7

 .= (( 1_ L) * ( - ( 1_ L))) by GROUP_1:def 7

 .= ( - ( 1_ L));

 then

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

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

 hence thesis;

 end;

 theorem :: HURWITZ:5



 Th5: for z be Element of F_Complex holds for k be Element of NAT holds ((( power F_Complex ) . (z,k)) *' ) = (( power F_Complex ) . ((z *' ),k))

 proof

 let z be Element of F_Complex , k be Element of NAT ;

 defpred P[ Nat] means ex j be Element of NAT st j = $1 & ((( power F_Complex ) . (z,j)) *' ) = (( power F_Complex ) . ((z *' ),j));

 A1:

 now

 let k be Nat;

 reconsider kk = k as Element of NAT by ORDINAL1:def 12;

 assume

 A2: P[k];

 ((( power F_Complex ) . (z,(k + 1))) *' ) = (((( power F_Complex ) . (z,kk)) * z) *' ) by GROUP_1:def 7

 .= ((( power F_Complex ) . ((z *' ),kk)) * (z *' )) by A2, COMPLFLD: 54

 .= (( power F_Complex ) . ((z *' ),(k + 1))) by GROUP_1:def 7;

 hence P[(k + 1)];

 end;

 ((( power F_Complex ) . (z, 0 )) *' ) = (( 1_ F_Complex ) *' ) by GROUP_1:def 7

 .= ( 1_ F_Complex ) by Lm2, COMPLEX1: 38

 .= (( power F_Complex ) . ((z *' ), 0 )) by GROUP_1:def 7;

 then

 A3: P[ 0 ];

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

 then ex j be Element of NAT st j = k & ((( power F_Complex ) . (z,j)) *' ) = (( power F_Complex ) . ((z *' ),j));

 hence thesis;

 end;

 theorem :: HURWITZ:6



 Th6: for F,G be FinSequence of F_Complex st ( len G) = ( len F) & for i be Element of NAT st i in ( dom G) holds (G /. i) = ((F /. i) *' ) holds ( Sum G) = (( Sum F) *' )

 proof

 defpred P[ Nat] means for F,G be FinSequence of F_Complex st ( len G) = ( len F) & ( len F) = $1 & for i be Element of NAT st i in ( dom G) holds (G /. i) = ((F /. i) *' ) holds ( Sum G) = (( Sum F) *' );

 let F,G be FinSequence of F_Complex ;

 assume that

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

 A2: for i be Element of NAT st i in ( dom G) holds (G /. i) = ((F /. i) *' );

 A3:

 now

 let k be Nat;

 assume

 A4: P[k];

 now

 let F,G be FinSequence of F_Complex ;

 assume that

 A5: ( len F) = ( len G) and

 A6: ( len F) = (k + 1) and

 A7: for i be Element of NAT st i in ( dom G) holds (G /. i) = ((F /. i) *' );

 set G1 = (G | ( Seg k));

 reconsider G1 as FinSequence by FINSEQ_1: 15;

 reconsider G1 as FinSequence of F_Complex by A5, A6, Lm1;



 A8: G = (G1 ^ <*(G /. (k + 1))*>) by A5, A6, Lm1;

 set F1 = (F | ( Seg k));

 reconsider F1 as FinSequence by FINSEQ_1: 15;

 reconsider F1 as FinSequence of F_Complex by A6, Lm1;



 A9: ( len F1) = k by A6, Lm1;



 A10: ( len G1) = k by A5, A6, Lm1;



 then

 A11: ( dom G1) = ( Seg ( len F1)) by A9, FINSEQ_1:def 3

 .= ( dom F1) by FINSEQ_1:def 3;

 1 <= (k + 1) by NAT_1: 11;

 then

 A12: (k + 1) in ( dom G) by A5, A6, FINSEQ_3: 25;



 A13: F = (F1 ^ <*(F /. (k + 1))*>) by A6, Lm1;



 A14: ( dom G) = ( Seg ( len F)) by A5, FINSEQ_1:def 3

 .= ( dom F) by FINSEQ_1:def 3;

 A15:

 now

 let i be Element of NAT ;

 assume

 A16: i in ( dom G1);



 A17: ( dom G1) c= ( dom G) by A5, A6, Lm1;



 then

 A18: (F /. i) = (F . i) by A14, A16, PARTFUN1:def 6

 .= (F1 . i) by A13, A11, A16, FINSEQ_1:def 7

 .= (F1 /. i) by A11, A16, PARTFUN1:def 6;



 thus (G1 /. i) = (G1 . i) by A16, PARTFUN1:def 6

 .= (G . i) by A8, A16, FINSEQ_1:def 7

 .= (G /. i) by A16, A17, PARTFUN1:def 6

 .= ((F1 /. i) *' ) by A7, A16, A17, A18;

 end;



 thus (( Sum F) *' ) = ((( Sum F1) + ( Sum <*(F /. (k + 1))*>)) *' ) by A13, RLVECT_1: 41

 .= ((( Sum F1) *' ) + (( Sum <*(F /. (k + 1))*>) *' )) by COMPLFLD: 51

 .= (( Sum G1) + (( Sum <*(F /. (k + 1))*>) *' )) by A4, A10, A9, A15

 .= (( Sum G1) + ((F /. (k + 1)) *' )) by RLVECT_1: 44

 .= (( Sum G1) + (G /. (k + 1))) by A7, A12

 .= (( Sum G1) + ( Sum <*(G /. (k + 1))*>)) by RLVECT_1: 44

 .= ( Sum G) by A8, RLVECT_1: 41;

 end;

 hence P[(k + 1)];

 end;

 now

 let F,G be FinSequence of F_Complex ;

 assume that

 A19: ( len F) = ( len G) and

 A20: ( len F) = 0 and for i be Element of NAT st i in ( dom G) holds (G /. i) = ((F /. i) *' );

 F = ( <*> the carrier of F_Complex ) by A20;

 then ( Sum F) = ( 0. F_Complex ) by RLVECT_1: 43;

 then

 A21: ( Sum F) = (( 0. F_Complex ) *' ) by Lm2, COMPLEX1: 38;

 G = ( <*> the carrier of F_Complex ) by A19, A20;

 hence ( Sum G) = (( Sum F) *' ) by A21, RLVECT_1: 43;

 end;

 then

 A22: P[ 0 ];

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

 hence thesis by A1, A2;

 end;

 theorem :: HURWITZ:7



 Th7: for L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, F1,F2 be FinSequence of L st ( len F1) = ( len F2) & for i be Element of NAT st i in ( dom F1) holds (F1 /. i) = ( - (F2 /. i)) holds ( Sum F1) = ( - ( Sum F2))

 proof

 let L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, F1,F2 be FinSequence of L;

 assume that

 A1: ( len F1) = ( len F2) and

 A2: for i be Element of NAT st i in ( dom F1) holds (F1 /. i) = ( - (F2 /. i));

 defpred P[ Nat] means for F1,F2 be FinSequence of L st ( len F1) = $1 & ( len F1) = ( len F2) & for i be Element of NAT st i in ( dom F1) holds (F1 /. i) = ( - (F2 /. i)) holds ( Sum F1) = ( - ( Sum F2));

 A3:

 now

 let k be Nat;

 assume

 A4: P[k];

 now

 let f,g be FinSequence of L;

 assume that

 A5: ( len f) = (k + 1) and

 A6: ( len f) = ( len g) and

 A7: for i be Element of NAT st i in ( dom f) holds (f /. i) = ( - (g /. i));

 set f1 = (f | ( Seg k)), g1 = (g | ( Seg k));

 reconsider f1, g1 as FinSequence by FINSEQ_1: 15;

 reconsider f1, g1 as FinSequence of L by A5, A6, Lm1;



 A8: ( len f1) = k by A5, Lm1;



 A9: ( len g1) = k by A5, A6, Lm1;



 then

 A10: ( dom f1) = ( Seg ( len g1)) by A8, FINSEQ_1:def 3

 .= ( dom g1) by FINSEQ_1:def 3;



 A11: f = (f1 ^ <*(f /. (k + 1))*>) by A5, Lm1;



 A12: g = (g1 ^ <*(g /. (k + 1))*>) by A5, A6, Lm1;

 A13:

 now



 A14: ( dom f1) c= ( dom f) by A5, Lm1;

 let i be Element of NAT ;

 assume

 A15: i in ( dom f1);

 ( dom g1) c= ( dom g) by A5, A6, Lm1;



 then

 A16: (g /. i) = (g . i) by A10, A15, PARTFUN1:def 6

 .= (g1 . i) by A12, A10, A15, FINSEQ_1:def 7

 .= (g1 /. i) by A10, A15, PARTFUN1:def 6;



 thus (f1 /. i) = (f1 . i) by A15, PARTFUN1:def 6

 .= (f . i) by A11, A15, FINSEQ_1:def 7

 .= (f /. i) by A15, A14, PARTFUN1:def 6

 .= ( - (g1 /. i)) by A7, A15, A14, A16;

 end;

 1 <= (k + 1) by NAT_1: 11;

 then

 A17: (k + 1) in ( dom f) by A5, FINSEQ_3: 25;



 thus ( Sum f) = (( Sum f1) + ( Sum <*(f /. (k + 1))*>)) by A11, RLVECT_1: 41

 .= (( - ( Sum g1)) + ( Sum <*(f /. (k + 1))*>)) by A4, A8, A9, A13

 .= (( - ( Sum g1)) + (f /. (k + 1))) by RLVECT_1: 44

 .= (( - ( Sum g1)) + ( - (g /. (k + 1)))) by A7, A17

 .= ( - (( Sum g1) + (g /. (k + 1)))) by RLVECT_1: 31

 .= ( - (( Sum g1) + ( Sum <*(g /. (k + 1))*>))) by RLVECT_1: 44

 .= ( - ( Sum g)) by A12, RLVECT_1: 41;

 end;

 hence P[(k + 1)];

 end;

 now

 let f,g be FinSequence of L;

 assume that

 A18: ( len f) = 0 and

 A19: ( len f) = ( len g) and for i be Element of NAT st i in ( dom f) holds (f /. i) = ( - (g /. i));



 A20: g = ( <*> the carrier of L) by A18, A19;

 f = ( <*> the carrier of L) by A18;



 hence ( Sum f) = ( 0. L) by RLVECT_1: 43

 .= ( - ( 0. L)) by RLVECT_1: 12

 .= ( - ( Sum g)) by A20, RLVECT_1: 43;

 end;

 then

 A21: P[ 0 ];

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

 hence thesis by A1, A2;

 end;

 theorem :: HURWITZ:8



 Th8: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for x be Element of L holds for F be FinSequence of L holds (x * ( Sum F)) = ( Sum (x * F))

 proof

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

 let x be Element of L;

 let F be FinSequence of L;

 defpred P[ Nat] means for x be Element of L, F be FinSequence of L st ( len F) = $1 holds (x * ( Sum F)) = ( Sum (x * F));



 A1: ex n be Element of NAT st ( len F) = n;

 A2:

 now

 let k be Nat;

 assume

 A3: P[k];

 now

 let x be Element of L;

 let F be FinSequence of L;

 set G = (F | ( Seg k));

 reconsider G as FinSequence by FINSEQ_1: 15;

 assume

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

 then

 reconsider G as FinSequence of L by Lm1;



 A5: ( len G) = k by A4, Lm1;



 A6: F = (G ^ <*(F /. (k + 1))*>) by A4, Lm1;



 thus (x * ( Sum F)) = (x * ( Sum (G ^ <*(F /. (k + 1))*>))) by A4, Lm1

 .= (x * (( Sum G) + ( Sum <*(F /. (k + 1))*>))) by RLVECT_1: 41

 .= ((x * ( Sum G)) + (x * ( Sum <*(F /. (k + 1))*>))) by VECTSP_1:def 2

 .= (( Sum (x * G)) + (x * ( Sum <*(F /. (k + 1))*>))) by A3, A5

 .= (( Sum (x * G)) + (x * (F /. (k + 1)))) by RLVECT_1: 44

 .= (( Sum (x * G)) + ( Sum <*(x * (F /. (k + 1)))*>)) by RLVECT_1: 44

 .= (( Sum (x * G)) + ( Sum (x * <*(F /. (k + 1))*>))) by POLYNOM1: 8

 .= ( Sum ((x * G) ^ (x * <*(F /. (k + 1))*>))) by RLVECT_1: 41

 .= ( Sum (x * F)) by A6, POLYNOM1: 10;

 end;

 hence P[(k + 1)];

 end;

 now

 let x be Element of L, F be FinSequence of L;

 assume

 A7: ( len F) = 0 ;

 ( Seg ( len (x * F))) = ( dom (x * F)) by FINSEQ_1:def 3

 .= ( dom F) by POLYNOM1:def 1

 .= ( Seg ( len F)) by FINSEQ_1:def 3;

 then ( len (x * F)) = 0 by A7;

 then

 A8: (x * F) = ( <*> the carrier of L);

 F = ( <*> the carrier of L) by A7;

 then ( Sum F) = ( 0. L) by RLVECT_1: 43;

 then (x * ( Sum F)) = ( 0. L);

 hence (x * ( Sum F)) = ( Sum (x * F)) by A8, RLVECT_1: 43;

 end;

 then

 A9: P[ 0 ];

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

 hence thesis by A1;

 end;

 begin



 Lm3: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be Polynomial of L holds ( - ( - p)) = p

 proof

 let L be add-associative right_zeroed right_complementable non empty addLoopStr;

 let p be Polynomial of L;

 A1:

 now

 let x be Nat;

 assume x < ( len p);



 thus (( - ( - p)) . x) = ( - (( - p) . x)) by BHSP_1: 44

 .= ( - ( - (p . x))) by BHSP_1: 44

 .= (p . x) by RLVECT_1: 17;

 end;

 ( len p) = ( len ( - p)) by POLYNOM4: 8

 .= ( len ( - ( - p))) by POLYNOM4: 8;

 hence thesis by A1, ALGSEQ_1: 12;

 end;

 theorem :: HURWITZ:9



 Th9: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds ( - ( 0_. L)) = ( 0_. L)

 proof

 let L be add-associative right_zeroed right_complementable non empty addLoopStr;

 set e = ( 0_. L), f = ( - ( 0_. L));



 A1: for x be Nat st x < ( len e) holds (e . x) = (f . x) by POLYNOM4: 3;

 ( len f) = ( len e) by POLYNOM4: 8;

 hence thesis by A1, ALGSEQ_1: 12;

 end;



 Lm4: for L be add-associative right_complementable right_zeroed distributive non empty doubleLoopStr, p be Polynomial of L holds for f be Element of ( Polynom-Ring L) holds f = p implies ( - f) = ( - p)

 proof

 let L be add-associative right_complementable right_zeroed distributive non empty doubleLoopStr, p be Polynomial of L;

 let f be Element of ( Polynom-Ring L);

 reconsider x = ( - p) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

 reconsider x as Element of ( Polynom-Ring L);

 assume f = p;



 then (f + x) = (p - p) by POLYNOM3:def 10

 .= ( 0_. L) by POLYNOM3: 29

 .= ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

 then f = ( - x) by RLVECT_1: 6;

 hence thesis by RLVECT_1: 17;

 end;

 theorem :: HURWITZ:10

 for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be Polynomial of L holds ( - ( - p)) = p by Lm3;

 theorem :: HURWITZ:11



 Th11: for L be add-associative right_zeroed right_complementable Abelian distributive non empty doubleLoopStr holds for p1,p2 be Polynomial of L holds ( - (p1 + p2)) = (( - p1) + ( - p2))

 proof

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

 let p1,p2 be Polynomial of L;

 reconsider p19 = p1, p29 = p2 as Element of ( Polynom-Ring L) by POLYNOM3:def 10;



 A1: ( - (p19 + p29)) = (( - p19) + ( - p29)) by RLVECT_1: 31;



 A2: ( - p2) = ( - p29) by Lm4;

 (p1 + p2) = (p19 + p29) by POLYNOM3:def 10;

 then

 A3: ( - (p1 + p2)) = ( - (p19 + p29)) by Lm4;

 ( - p1) = ( - p19) by Lm4;

 hence thesis by A3, A2, A1, POLYNOM3:def 10;

 end;

 theorem :: HURWITZ:12



 Th12: for L be add-associative right_zeroed right_complementable distributive Abelian non empty doubleLoopStr holds for p1,p2 be Polynomial of L holds ( - (p1 *' p2)) = (( - p1) *' p2) & ( - (p1 *' p2)) = (p1 *' ( - p2))

 proof

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

 let p1,p2 be Polynomial of L;

 reconsider p19 = p1, p29 = p2 as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

 (p1 *' p2) = (p19 * p29) by POLYNOM3:def 10;

 then

 A1: ( - (p1 *' p2)) = ( - (p19 * p29)) by Lm4;

 ( - p1) = ( - p19) by Lm4;

 then (( - p1) *' p2) = (( - p19) * p29) by POLYNOM3:def 10;

 hence ( - (p1 *' p2)) = (( - p1) *' p2) by A1, VECTSP_1: 9;

 ( - p2) = ( - p29) by Lm4;

 then (p1 *' ( - p2)) = (p19 * ( - p29)) by POLYNOM3:def 10;

 hence thesis by A1, VECTSP_1: 8;

 end;

 definition

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

 let F be FinSequence of ( Polynom-Ring L);

 let i be Element of NAT ;

 :: HURWITZ:def1

 func Coeff (F,i) -> FinSequence of L means

 : Def1: ( len it ) = ( len F) & for j be Element of NAT st j in ( dom it ) holds ex p be Polynomial of L st p = (F . j) & (it . j) = (p . i);

 existence

 proof

 defpred P[ set, set] means ex p be Polynomial of L st p = (F . $1) & $2 = (p . i);



 A1: for k be Nat st k in ( Seg ( len F)) holds ex x be Element of the carrier of L st P[k, x]

 proof

 let k be Nat;

 assume

 A2: k in ( Seg ( len F));

 reconsider t = (F /. k) as Polynomial of L by POLYNOM3:def 10;

 take (t . i);

 take t;

 k in ( dom F) by A2, FINSEQ_1:def 3;

 hence t = (F . k) by PARTFUN1:def 6;

 thus thesis;

 end;

 consider G be FinSequence of L such that

 A3: ( dom G) = ( Seg ( len F)) & for k be Nat st k in ( Seg ( len F)) holds P[k, (G . k)] from FINSEQ_1:sch 5( A1);

 take G;

 thus ( len G) = ( len F) by A3, FINSEQ_1:def 3;

 thus thesis by A3;

 end;

 uniqueness

 proof

 let z1,z2 be FinSequence of L;

 assume that

 A4: ( len z1) = ( len F) and

 A5: for j be Element of NAT st j in ( dom z1) holds ex p be Polynomial of L st p = (F . j) & (z1 . j) = (p . i);

 assume that

 A6: ( len z2) = ( len F) and

 A7: for j be Element of NAT st j in ( dom z2) holds ex p be Polynomial of L st p = (F . j) & (z2 . j) = (p . i);



 A8: ( dom z1) = ( Seg ( len F)) by A4, FINSEQ_1:def 3

 .= ( dom z2) by A6, FINSEQ_1:def 3;

 now

 let k be Nat;

 assume

 A9: k in ( dom z1);

 then

 A10: ex p1 be Polynomial of L st p1 = (F . k) & (z1 . k) = (p1 . i) by A5;

 ex p2 be Polynomial of L st p2 = (F . k) & (z2 . k) = (p2 . i) by A7, A8, A9;

 hence (z1 . k) = (z2 . k) by A10;

 end;

 hence thesis by A8, FINSEQ_1: 13;

 end;

 end

 theorem :: HURWITZ:13



 Th13: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for p be Polynomial of L holds for F be FinSequence of ( Polynom-Ring L) st p = ( Sum F) holds for i be Element of NAT holds (p . i) = ( Sum ( Coeff (F,i)))

 proof

 let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Polynomial of L;

 let F be FinSequence of ( Polynom-Ring L);

 assume

 A1: p = ( Sum F);

 defpred P[ Nat] means for p be Polynomial of L holds for F be FinSequence of ( Polynom-Ring L) st p = ( Sum F) & ( len F) = $1 holds for i be Element of NAT holds (p . i) = ( Sum ( Coeff (F,i)));

 let i be Element of NAT ;



 A2: ex m be Nat st ( len F) = m;

 A3:

 now

 let k be Nat;

 assume

 A4: P[k];

 now

 let p be Polynomial of L;

 let F be FinSequence of ( Polynom-Ring L);

 assume that

 A5: p = ( Sum F) and

 A6: ( len F) = (k + 1);

 reconsider rf = (F /. (k + 1)) as Polynomial of L by POLYNOM3:def 10;

 let i be Element of NAT ;

 set G = (F | ( Seg k));

 reconsider G as FinSequence by FINSEQ_1: 15;

 reconsider G as FinSequence of ( Polynom-Ring L) by A6, Lm1;



 A7: ( len G) = k by A6, Lm1;



 A8: k <= ( len F) by A6, NAT_1: 13;

 A9:

 now



 A10: ( dom ( Coeff (G,i))) = ( Seg ( len ( Coeff (G,i)))) by FINSEQ_1:def 3

 .= ( Seg ( len G)) by Def1

 .= ( dom G) by FINSEQ_1:def 3;

 let j be Nat;

 assume

 A11: j in ( dom ( Coeff (F,i)));

 per cases ;

 suppose

 A12: j in ( dom ( Coeff (G,i)));

 then

 A13: ((( Coeff (G,i)) ^ <*(rf . i)*>) . j) = (( Coeff (G,i)) . j) by FINSEQ_1:def 7;



 A14: ex p be Polynomial of L st p = (F . j) & (( Coeff (F,i)) . j) = (p . i) by A11, Def1;

 ex p1 be Polynomial of L st p1 = (G . j) & (( Coeff (G,i)) . j) = (p1 . i) by A12, Def1;

 hence (( Coeff (F,i)) . j) = ((( Coeff (G,i)) ^ <*(rf . i)*>) . j) by A10, A12, A13, A14, FUNCT_1: 47;

 end;

 suppose

 A15: not j in ( dom ( Coeff (G,i)));



 A16: ( dom ( Coeff (F,i))) = ( Seg ( len ( Coeff (F,i)))) by FINSEQ_1:def 3

 .= ( Seg ( len F)) by Def1;

 then

 A17: 1 <= j by A11, FINSEQ_1: 1;

 A18:

 now

 assume j < (k + 1);

 then j <= k by NAT_1: 13;

 then j in ( Seg k) by A17;

 hence contradiction by A8, A10, A15, FINSEQ_1: 17;

 end;

 j <= (k + 1) by A6, A11, A16, FINSEQ_1: 1;

 then

 A19: j = (k + 1) by A18, XXREAL_0: 1;

 ( dom <*(rf . i)*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

 then

 A20: 1 in ( dom <*(rf . i)*>) by TARSKI:def 1;

 1 <= (k + 1) by NAT_1: 11;

 then

 A21: (k + 1) in ( dom F) by A6, FINSEQ_3: 25;



 A22: ex p be Polynomial of L st p = (F . j) & (( Coeff (F,i)) . j) = (p . i) by A11, Def1;

 ( len ( Coeff (G,i))) = k by A7, Def1;



 then ((( Coeff (G,i)) ^ <*(rf . i)*>) . j) = ( <*(rf . i)*> . 1) by A19, A20, FINSEQ_1:def 7

 .= (rf . i) by FINSEQ_1: 40;

 hence (( Coeff (F,i)) . j) = ((( Coeff (G,i)) ^ <*(rf . i)*>) . j) by A19, A22, A21, PARTFUN1:def 6;

 end;

 end;

 ( len (( Coeff (G,i)) ^ <*(rf . i)*>)) = (( len ( Coeff (G,i))) + ( len <*(rf . i)*>)) by FINSEQ_1: 22

 .= (( len ( Coeff (G,i))) + 1) by FINSEQ_1: 39

 .= (k + 1) by A7, Def1

 .= ( len ( Coeff (F,i))) by A6, Def1;



 then ( dom ( Coeff (F,i))) = ( Seg ( len (( Coeff (G,i)) ^ <*(rf . i)*>))) by FINSEQ_1:def 3

 .= ( dom (( Coeff (G,i)) ^ <*(rf . i)*>)) by FINSEQ_1:def 3;

 then

 A23: ( Coeff (F,i)) = (( Coeff (G,i)) ^ <*(rf . i)*>) by A9, FINSEQ_1: 13;

 reconsider pg = ( Sum G) as Polynomial of L by POLYNOM3:def 10;

 F = (G ^ <*(F /. (k + 1))*>) by A6, Lm1;



 then ( Sum F) = (( Sum G) + ( Sum <*(F /. (k + 1))*>)) by RLVECT_1: 41

 .= (( Sum G) + (F /. (k + 1))) by RLVECT_1: 44

 .= (pg + rf) by POLYNOM3:def 10;



 hence (p . i) = ((pg . i) + (rf . i)) by A5, NORMSP_1:def 2

 .= (( Sum ( Coeff (G,i))) + (rf . i)) by A4, A7

 .= (( Sum ( Coeff (G,i))) + ( Sum <*(rf . i)*>)) by RLVECT_1: 44

 .= ( Sum ( Coeff (F,i))) by A23, RLVECT_1: 41;

 end;

 hence P[(k + 1)];

 end;

 now

 let p be Polynomial of L;

 let F be FinSequence of ( Polynom-Ring L);

 assume that

 A24: p = ( Sum F) and

 A25: ( len F) = 0 ;

 let i be Element of NAT ;

 F = ( <*> the carrier of ( Polynom-Ring L)) by A25;

 then ( Sum F) = ( 0. ( Polynom-Ring L)) by RLVECT_1: 43;

 then p = ( 0_. L) by A24, POLYNOM3:def 10;

 then

 A26: (p . i) = ( 0. L);

 ( len ( Coeff (F,i))) = 0 by A25, Def1;

 then ( Coeff (F,i)) = ( <*> the carrier of L);

 hence (p . i) = ( Sum ( Coeff (F,i))) by A26, RLVECT_1: 43;

 end;

 then

 A27: P[ 0 ];

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

 hence thesis by A1, A2;

 end;



 Lm5: for L be add-associative right_zeroed right_complementable distributive Abelian non empty doubleLoopStr holds for p1,p2 be Polynomial of L holds for p29 be Element of ( Polynom-Ring L) st p29 = p2 holds for F be FinSequence of ( Polynom-Ring L) st p1 = ( Sum F) holds (p2 *' p1) = ( Sum (p29 * F))

 proof

 let L be add-associative right_zeroed right_complementable distributive Abelian non empty doubleLoopStr, p1,p2 be Polynomial of L;

 let p29 be Element of ( Polynom-Ring L);

 assume

 A1: p29 = p2;

 reconsider p19 = p1 as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

 let F be FinSequence of ( Polynom-Ring L);

 assume p1 = ( Sum F);

 then (p29 * p19) = ( Sum (p29 * F)) by Th8;

 hence thesis by A1, POLYNOM3:def 10;

 end;

 theorem :: HURWITZ:14



 Th14: for L be associative non empty doubleLoopStr holds for p be Polynomial of L holds for x1,x2 be Element of L holds (x1 * (x2 * p)) = ((x1 * x2) * p)

 proof

 let L be associative non empty doubleLoopStr, p be Polynomial of L;

 let x1,x2 be Element of L;

 set f = (x1 * (x2 * p)), g = ((x1 * x2) * p);

 A1:

 now

 let i9 be object;

 assume i9 in ( dom f);

 then

 reconsider i = i9 as Element of NAT ;

 (f . i) = (x1 * ((x2 * p) . i)) by POLYNOM5:def 4

 .= (x1 * (x2 * (p . i))) by POLYNOM5:def 4

 .= ((x1 * x2) * (p . i)) by GROUP_1:def 3

 .= (g . i) by POLYNOM5:def 4;

 hence (f . i9) = (g . i9);

 end;

 ( dom f) = NAT by FUNCT_2:def 1

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

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:15



 Th15: for L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr holds for p be Polynomial of L holds for x be Element of L holds ( - (x * p)) = (( - x) * p)

 proof

 let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, p be Polynomial of L;

 let x be Element of L;

 set f = ( - (x * p)), g = (( - x) * p);

 A1:

 now

 let i9 be object;

 assume i9 in ( dom f);

 then

 reconsider i = i9 as Element of NAT ;

 (f . i) = ( - ((x * p) . i)) by BHSP_1: 44

 .= ( - (x * (p . i))) by POLYNOM5:def 4

 .= (( - x) * (p . i)) by VECTSP_1: 9

 .= (g . i) by POLYNOM5:def 4;

 hence (f . i9) = (g . i9);

 end;

 ( dom f) = NAT by FUNCT_2:def 1

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

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:16



 Th16: for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for p be Polynomial of L holds for x be Element of L holds ( - (x * p)) = (x * ( - p))

 proof

 let L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, p be Polynomial of L;

 let x be Element of L;

 set f = ( - (x * p)), g = (x * ( - p));

 A1:

 now

 let i9 be object;

 assume i9 in ( dom f);

 then

 reconsider i = i9 as Element of NAT ;

 (f . i) = ( - ((x * p) . i)) by BHSP_1: 44

 .= ( - (x * (p . i))) by POLYNOM5:def 4

 .= (x * ( - (p . i))) by VECTSP_1: 8

 .= (x * (( - p) . i)) by BHSP_1: 44

 .= (g . i) by POLYNOM5:def 4;

 hence (f . i9) = (g . i9);

 end;

 ( dom f) = NAT by FUNCT_2:def 1

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

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:17



 Th17: for L be left-distributive non empty doubleLoopStr holds for p be Polynomial of L holds for x1,x2 be Element of L holds ((x1 + x2) * p) = ((x1 * p) + (x2 * p))

 proof

 let L be left-distributive non empty doubleLoopStr, p be Polynomial of L;

 let x1,x2 be Element of L;

 set f = ((x1 + x2) * p), g = ((x1 * p) + (x2 * p));

 A1:

 now

 let i9 be object;

 assume i9 in ( dom f);

 then

 reconsider i = i9 as Element of NAT ;

 (f . i) = ((x1 + x2) * (p . i)) by POLYNOM5:def 4

 .= ((x1 * (p . i)) + (x2 * (p . i))) by VECTSP_1:def 3

 .= (((x1 * p) . i) + (x2 * (p . i))) by POLYNOM5:def 4

 .= (((x1 * p) . i) + ((x2 * p) . i)) by POLYNOM5:def 4

 .= (g . i) by NORMSP_1:def 2;

 hence (f . i9) = (g . i9);

 end;

 ( dom f) = NAT by FUNCT_2:def 1

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

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:18



 Th18: for L be right-distributive non empty doubleLoopStr holds for p1,p2 be Polynomial of L holds for x be Element of L holds (x * (p1 + p2)) = ((x * p1) + (x * p2))

 proof

 let L be right-distributive non empty doubleLoopStr, p1,p2 be Polynomial of L;

 let x be Element of L;

 set f = (x * (p1 + p2)), g = ((x * p1) + (x * p2));

 A1:

 now

 let i9 be object;

 assume i9 in ( dom f);

 then

 reconsider i = i9 as Element of NAT ;

 (f . i) = (x * ((p1 + p2) . i)) by POLYNOM5:def 4

 .= (x * ((p1 . i) + (p2 . i))) by NORMSP_1:def 2

 .= ((x * (p1 . i)) + (x * (p2 . i))) by VECTSP_1:def 2

 .= (((x * p1) . i) + (x * (p2 . i))) by POLYNOM5:def 4

 .= (((x * p1) . i) + ((x * p2) . i)) by POLYNOM5:def 4

 .= (g . i) by NORMSP_1:def 2;

 hence (f . i9) = (g . i9);

 end;

 ( dom f) = NAT by FUNCT_2:def 1

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

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:19



 Th19: for L be add-associative right_zeroed right_complementable distributive commutative associative non empty doubleLoopStr holds for p1,p2 be Polynomial of L holds for x be Element of L holds (p1 *' (x * p2)) = (x * (p1 *' p2))

 proof

 let L be add-associative right_zeroed right_complementable distributive commutative associative non empty doubleLoopStr, p1,p2 be Polynomial of L;

 let x be Element of L;

 set f = (p1 *' (x * p2)), g = (x * (p1 *' p2));

 A1:

 now

 let i9 be object;

 assume i9 in ( dom f);

 then

 reconsider i = i9 as Element of NAT ;

 consider rf be FinSequence of L such that

 A2: ( len rf) = (i + 1) and

 A3: (f . i) = ( Sum rf) and

 A4: for k be Element of NAT st k in ( dom rf) holds (rf . k) = ((p1 . (k -' 1)) * ((x * p2) . ((i + 1) -' k))) by POLYNOM3:def 9;

 consider rp be FinSequence of L such that

 A5: ( len rp) = (i + 1) and

 A6: ((p1 *' p2) . i) = ( Sum rp) and

 A7: for k be Element of NAT st k in ( dom rp) holds (rp . k) = ((p1 . (k -' 1)) * (p2 . ((i + 1) -' k))) by POLYNOM3:def 9;



 A8: ( Seg ( len (x * rp))) = ( dom (x * rp)) by FINSEQ_1:def 3

 .= ( dom rp) by POLYNOM1:def 1

 .= ( Seg ( len rp)) by FINSEQ_1:def 3;



 then

 A9: ( dom (x * rp)) = ( Seg ( len rf)) by A2, A5, FINSEQ_1:def 3

 .= ( dom rf) by FINSEQ_1:def 3;



 A10: ( dom (x * rp)) = ( dom rp) by POLYNOM1:def 1;

 A11:

 now

 let j be Nat;

 assume that

 A12: 1 <= j and

 A13: j <= ( len rf);



 A14: j in ( dom rf) by A12, A13, FINSEQ_3: 25;

 then

 A15: (rp /. j) = (rp . j) by A9, A10, PARTFUN1:def 6;



 thus ((x * rp) . j) = ((x * rp) /. j) by A9, A14, PARTFUN1:def 6

 .= (x * (rp /. j)) by A9, A10, A14, POLYNOM1:def 1

 .= (x * ((p1 . (j -' 1)) * (p2 . ((i + 1) -' j)))) by A7, A9, A10, A14, A15

 .= ((p1 . (j -' 1)) * (x * (p2 . ((i + 1) -' j)))) by GROUP_1:def 3

 .= ((p1 . (j -' 1)) * ((x * p2) . ((i + 1) -' j))) by POLYNOM5:def 4

 .= (rf . j) by A4, A14;

 end;

 (g . i) = (x * ( Sum rp)) by A6, POLYNOM5:def 4

 .= ( Sum (x * rp)) by Th8

 .= (f . i) by A2, A3, A5, A8, A11, FINSEQ_1: 6, FINSEQ_1: 14;

 hence (f . i9) = (g . i9);

 end;

 ( dom f) = NAT by FUNCT_2:def 1

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

 hence thesis by A1, FUNCT_1: 2;

 end;

 definition

 let L be non empty ZeroStr;

 let p be Polynomial of L;

 :: HURWITZ:def2

 func degree p -> Integer equals (( len p) - 1);

 coherence ;

 end

 notation

 let L be non empty ZeroStr;

 let p be Polynomial of L;

 synonym deg p for degree p;

 end



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

 proof

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

 assume ( len s) > 0 ;

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

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

 then

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

 assume

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

 now

 let i be Nat;

 assume

 A2: i >= l;

 per cases by A2, XXREAL_0: 1;

 suppose i = l;

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

 end;

 suppose i > l;

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

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

 end;

 end;

 then

 A3: l is_at_least_length_of s by ALGSEQ_1:def 2;

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

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

 hence contradiction by A3, ALGSEQ_1:def 3;

 end;

 theorem :: HURWITZ:20



 Th20: for L be non empty ZeroStr holds for p be Polynomial of L holds ( deg p) = ( - 1) iff p = ( 0_. L)

 proof

 let L be non empty ZeroStr;

 let p be Polynomial of L;

 now

 assume p = ( 0_. L);

 then ( len p) = 0 by POLYNOM4: 3;

 hence ( deg p) = ( - 1);

 end;

 hence thesis by POLYNOM4: 5;

 end;



 Lm7: for L be non empty ZeroStr, p be Polynomial of L holds ( deg p) <> ( - 1) implies (p . ( deg p)) <> ( 0. L)

 proof

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

 assume ( deg p) <> ( - 1);

 then ( len p) <> 0 ;

 hence thesis by Lm6;

 end;



 Lm8: for L be non empty ZeroStr holds for p be Polynomial of L holds ( deg p) is Element of NAT iff p <> ( 0_. L)

 proof

 let L be non empty ZeroStr;

 let p be Polynomial of L;

 now

 assume p <> ( 0_. L);

 then ( len p) <> 0 by POLYNOM4: 5;

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

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

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

 hence ( deg p) is Element of NAT by INT_1: 3;

 end;

 hence thesis by Th20;

 end;

 theorem :: HURWITZ:21

 for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p1,p2 be Polynomial of L st ( deg p1) <> ( deg p2) holds ( deg (p1 + p2)) = ( max (( deg p1),( deg p2)))

 proof

 let L be add-associative right_zeroed right_complementable non empty addLoopStr;

 let p1,p2 be Polynomial of L;

 assume ( deg p1) <> ( deg p2);

 then

 A1: ( deg (p1 + p2)) = (( max (( len p1),( len p2))) - 1) by POLYNOM4: 7;

 per cases by XXREAL_0: 16;

 suppose

 A2: ( max (( len p1),( len p2))) = ( len p1);

 then ( len p2) <= ( len p1) by XXREAL_0: 25;

 then ( deg p2) <= ( deg p1) by XREAL_1: 9;

 hence thesis by A1, A2, XXREAL_0:def 10;

 end;

 suppose

 A3: ( max (( len p1),( len p2))) = ( len p2);

 then ( len p1) <= ( len p2) by XXREAL_0: 25;

 then ( deg p1) <= ( deg p2) by XREAL_1: 9;

 hence thesis by A1, A3, XXREAL_0:def 10;

 end;

 end;



 Lm9: for L be non empty ZeroStr, p be Polynomial of L holds ( deg p) >= ( - 1)

 proof

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

 per cases ;

 suppose p = ( 0_. L);

 hence thesis by Th20;

 end;

 suppose p <> ( 0_. L);

 hence thesis by Lm8;

 end;

 end;

 theorem :: HURWITZ:22



 Th22: for L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr holds for p1,p2 be Polynomial of L holds ( deg (p1 + p2)) <= ( max (( deg p1),( deg p2)))

 proof

 let L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr;

 let p1,p2 be Polynomial of L;

 per cases ;

 suppose

 A1: p1 = ( 0_. L);

 then ( deg p1) = ( - 1) by Th20;

 then

 A2: ( deg p2) >= ( deg p1) by Lm9;

 ( deg (p1 + p2)) = ( deg p2) by A1, POLYNOM3: 28

 .= ( max (( deg p1),( deg p2))) by A2, XXREAL_0:def 10;

 hence thesis;

 end;

 suppose

 A3: p2 = ( 0_. L);

 then ( deg p2) = ( - 1) by Th20;

 then

 A4: ( deg p1) >= ( deg p2) by Lm9;

 ( deg (p1 + p2)) = ( deg p1) by A3, POLYNOM3: 28

 .= ( max (( deg p1),( deg p2))) by A4, XXREAL_0:def 10;

 hence thesis;

 end;

 suppose

 A5: p1 <> ( 0_. L) & p2 <> ( 0_. L);

 then

 A6: ( deg p2) is Element of NAT by Lm8;

 ( deg p1) is Element of NAT by A5, Lm8;

 then

 reconsider m = ( max (( deg p1),( deg p2))) as Element of NAT by A6, XXREAL_0: 16;

 for k be Nat st k >= (m + 1) holds ((p1 + p2) . k) = ( 0. L)

 proof

 let k be Nat;

 assume

 A7: k >= (m + 1);

 ( deg p2) <= m by XXREAL_0: 25;

 then (( deg p2) + 1) <= (m + 1) by XREAL_1: 6;

 then

 A8: (p2 . k) = ( 0. L) by A7, ALGSEQ_1: 8, XXREAL_0: 2;

 ( deg p1) <= m by XXREAL_0: 25;

 then (( deg p1) + 1) <= (m + 1) by XREAL_1: 6;

 then (p1 . k) = ( 0. L) by A7, ALGSEQ_1: 8, XXREAL_0: 2;



 hence ((p1 + p2) . k) = (( 0. L) + ( 0. L)) by A8, NORMSP_1:def 2

 .= ( 0. L) by RLVECT_1:def 4;

 end;

 then (m + 1) is_at_least_length_of (p1 + p2) by ALGSEQ_1:def 2;

 then ( len (p1 + p2)) <= (m + 1) by ALGSEQ_1:def 3;

 then (( len (p1 + p2)) - 1) <= ((m + 1) - 1) by XREAL_1: 9;

 hence thesis;

 end;

 end;

 theorem :: HURWITZ:23



 Th23: for L be add-associative right_zeroed right_complementable distributive associative well-unital domRing-like non empty doubleLoopStr holds for p1,p2 be Polynomial of L st p1 <> ( 0_. L) & p2 <> ( 0_. L) holds ( deg (p1 *' p2)) = (( deg p1) + ( deg p2))

 proof

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

 let p1,p2 be Polynomial of L;

 assume that

 A1: p1 <> ( 0_. L) and

 A2: p2 <> ( 0_. L);



 A3: ( dom p2) = NAT by FUNCT_2:def 1;

 ( deg p2) is Element of NAT by A2, Lm8;

 then

 A4: (p2 /. ( deg p2)) = (p2 . ( deg p2)) by A3, PARTFUN1:def 6;

 ( deg p2) <> ( - 1) by A2, Th20;

 then

 A5: (p2 /. ( deg p2)) <> ( 0. L) by A4, Lm7;



 A6: ( dom p1) = NAT by FUNCT_2:def 1;

 ( deg p1) is Element of NAT by A1, Lm8;

 then

 A7: (p1 /. ( deg p1)) = (p1 . ( deg p1)) by A6, PARTFUN1:def 6;

 ( len p2) <> 0 by A2, POLYNOM4: 5;

 then (( len p2) + 1) > ( 0 + 1) by XREAL_1: 6;

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

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

 then

 A8: (p2 /. ( deg p2)) = (p2 . (( len p2) -' 1)) by A4, XREAL_0:def 2;

 ( deg p1) <> ( - 1) by A1, Th20;

 then

 A9: (p1 /. ( deg p1)) <> ( 0. L) by A7, Lm7;

 ( len p1) <> 0 by A1, POLYNOM4: 5;

 then (( len p1) + 1) > ( 0 + 1) by XREAL_1: 6;

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

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

 then (p1 /. ( deg p1)) = (p1 . (( len p1) -' 1)) by A7, XREAL_0:def 2;

 then ((p1 . (( len p1) -' 1)) * (p2 . (( len p2) -' 1))) <> ( 0. L) by A8, A9, A5, VECTSP_2:def 1;



 hence ( deg (p1 *' p2)) = (((( len p1) + ( len p2)) - 1) - 1) by POLYNOM4: 10

 .= (( deg p1) + ( deg p2));

 end;

 theorem :: HURWITZ:24



 Th24: for L be add-associative right_zeroed right_complementable unital non empty doubleLoopStr holds for p be Polynomial of L st ( deg p) = 0 holds not (p is with_roots)

 proof

 let L be add-associative right_zeroed right_complementable unital non empty doubleLoopStr, p be Polynomial of L;

 assume

 A1: ( deg p) = 0 ;

 then

 A2: p = <%(p . 0 )%> by ALGSEQ_1:def 5;

 now

 assume p is with_roots;

 then

 consider x be Element of L such that

 A3: x is_a_root_of p by POLYNOM5:def 8;

 ( 0. L) = ( eval (p,x)) by A3, POLYNOM5:def 7

 .= (p . 0 ) by A2, POLYNOM5: 37;

 hence contradiction by A1, A2, ALGSEQ_1: 14;

 end;

 hence thesis;

 end;



 Lm10: for L be unital non empty doubleLoopStr holds for z be Element of L, k be Element of NAT st k <> 0 holds ((( 0_. L) +* (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L)))) . 0 ) = ( - (( power L) . (z,k))) & ((( 0_. L) +* (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L)))) . k) = ( 1_ L)

 proof

 let L be unital non empty doubleLoopStr;

 let z be Element of L;

 let k be Element of NAT ;

 assume

 A1: k <> 0 ;

 set t = (( 0_. L) +* (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L)))), f = (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L))), a = ( - (( power L) . (z,k)));



 A2: ( dom f) = { 0 , k} by FUNCT_4: 62;

 now

 let u be object;

 assume u in { 0 , k};

 then u = 0 or u = k by TARSKI:def 2;

 hence u in NAT ;

 end;

 then

 A3: { 0 , k} c= NAT by TARSKI:def 3;



 A4: (( dom ( 0_. L)) \/ ( dom f)) = NAT by A2, A3, XBOOLE_1: 12;

 0 in ( dom f) by A2, TARSKI:def 2;



 hence (t . 0 ) = (f . 0 ) by A4, FUNCT_4:def 1

 .= a by A1, FUNCT_4: 63;

 k in ( dom f) by A2, TARSKI:def 2;



 hence (t . k) = (f . k) by A4, FUNCT_4:def 1

 .= ( 1_ L) by FUNCT_4: 63;

 end;



 Lm11: for L be unital non empty doubleLoopStr holds for z be Element of L, k be Element of NAT , i be Nat st i <> 0 & i <> k holds ((( 0_. L) +* (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L)))) . i) = ( 0. L)

 proof

 let L be unital non empty doubleLoopStr;

 let z be Element of L, k be Element of NAT , i be Nat;

 assume that

 A1: i <> 0 and

 A2: i <> k;

 set t = (( 0_. L) +* (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L)))), f = (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L)));

 now

 let u be object;

 assume u in { 0 , k};

 then u = 0 or u = k by TARSKI:def 2;

 hence u in NAT ;

 end;

 then

 A4: { 0 , k} c= NAT by TARSKI:def 3;

 ( dom f) = { 0 , k} by FUNCT_4: 62;

 then

 A5: (( dom ( 0_. L)) \/ ( dom f)) = NAT by A4, XBOOLE_1: 12;



 A6: i in NAT by ORDINAL1:def 12;

 not i in ( dom f) by A1, A2, TARSKI:def 2;



 hence (t . i) = (( 0_. L) . i) by A5, A6, FUNCT_4:def 1

 .= ( 0. L) by A6, FUNCOP_1: 7;

 end;

 definition

 let L be unital non empty doubleLoopStr;

 let z be Element of L;

 let k be Element of NAT ;

 :: HURWITZ:def3

 func rpoly (k,z) -> Polynomial of L equals (( 0_. L) +* (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L))));

 coherence

 proof

 now

 let u be object;

 assume u in { 0 , k};

 then u = 0 or u = k by TARSKI:def 2;

 hence u in NAT ;

 end;

 then

 A1: { 0 , k} c= NAT by TARSKI:def 3;

 set a = ( - (( power L) . (z,k)));

 set p = (( 0_. L) +* (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L))));

 set f = (( 0 ,k) --> (( - (( power L) . (z,k))),( 1_ L)));



 A2: ( dom f) = { 0 , k} by FUNCT_4: 62;



 A3: k in {k} by TARSKI:def 1;

 then

 A4: k in ( dom ( {k} --> ( 1_ L)));

 A5:

 now

 let x9 be object;

 assume x9 in NAT ;

 then

 reconsider x = x9 as Element of NAT ;

 per cases ;

 suppose

 A6: k = 0 & x = 0 ;

 then x in ( dom f) by A2, TARSKI:def 2;



 then (p . x) = (f . x) by FUNCT_4: 13

 .= ((( 0 .--> a) +* (k .--> ( 1_ L))) . x) by FUNCT_4:def 4

 .= ((k .--> ( 1_ L)) . x) by A4, A6, FUNCT_4: 13

 .= ( 1_ L) by A3, A6, FUNCOP_1: 7;

 hence (p . x9) in the carrier of L;

 end;

 suppose x = 0 & k <> 0 ;

 then (p . x) = ( - (( power L) . (z,k))) by Lm10;

 hence (p . x9) in the carrier of L;

 end;

 suppose x = k & k <> 0 ;

 then (p . x) = ( 1_ L) by Lm10;

 hence (p . x9) in the carrier of L;

 end;

 suppose x <> 0 & x <> k;

 then (p . x) = ( 0. L) by Lm11;

 hence (p . x9) in the carrier of L;

 end;

 end;

 (( dom ( 0_. L)) \/ ( dom f)) = NAT by A2, A1, XBOOLE_1: 12;

 then ( dom p) = NAT by FUNCT_4:def 1;

 then

 reconsider p as sequence of the carrier of L by A5, FUNCT_2: 3;

 reconsider p as sequence of L;

 now

 let i be Nat;

 assume

 A7: i >= (k + 1);

 then i <> k by NAT_1: 13;

 hence (p . i) = ( 0. L) by A7, Lm11;

 end;

 then

 reconsider p as AlgSequence of L by ALGSEQ_1:def 1;

 p is Polynomial of L;

 hence thesis;

 end;

 end

 theorem :: HURWITZ:25

 for L be unital non empty doubleLoopStr holds for z be Element of L holds for k be Element of NAT st k <> 0 holds (( rpoly (k,z)) . 0 ) = ( - (( power L) . (z,k))) & (( rpoly (k,z)) . k) = ( 1_ L) by Lm10;

 theorem :: HURWITZ:26

 for L be unital non empty doubleLoopStr holds for z be Element of L holds for i,k be Element of NAT st i <> 0 & i <> k holds (( rpoly (k,z)) . i) = ( 0. L) by Lm11;

 theorem :: HURWITZ:27



 Th27: for L be well-unital non degenerated non empty doubleLoopStr holds for z be Element of L holds for k be Element of NAT holds ( deg ( rpoly (k,z))) = k

 proof

 let L be well-unital non degenerated non empty doubleLoopStr;

 let z be Element of L;

 let k be Element of NAT ;

 set t = ( rpoly (k,z));

 set a = ( - (( power L) . (z,k)));

 set f = (( 0 ,k) --> (a,( 1_ L)));

 per cases ;

 suppose

 A1: k = 0 ;

 A2:

 now

 let m be Nat;

 assume

 A3: m is_at_least_length_of t;

 now

 assume m < 1;

 then

 A4: m = 0 by NAT_1: 14;



 A5: k in {k} by TARSKI:def 1;

 then

 A6: k in ( dom ( {k} --> ( 1_ L)));

 ( dom f) = { 0 , k} by FUNCT_4: 62;

 then 0 in ( dom f) by TARSKI:def 2;



 then (t . 0 ) = (f . 0 ) by FUNCT_4: 13

 .= ((( 0 .--> a) +* (k .--> ( 1_ L))) . 0 ) by FUNCT_4:def 4

 .= (( 0 .--> ( 1_ L)) . 0 ) by A1, A6, FUNCT_4: 13

 .= ( 1_ L) by A1, A5, FUNCOP_1: 7;

 hence contradiction by A3, A4, ALGSEQ_1:def 2;

 end;

 hence 1 <= m;

 end;

 now

 let i be Nat;



 A7: i in NAT by ORDINAL1:def 12;

 assume i >= 1;

 then not i in ( dom f) by A1, TARSKI:def 2;



 hence (t . i) = (( 0_. L) . i) by FUNCT_4: 11

 .= ( 0. L) by A7, FUNCOP_1: 7;

 end;

 then 1 is_at_least_length_of t by ALGSEQ_1:def 2;

 then ( len ( rpoly (k,z))) = 1 by A2, ALGSEQ_1:def 3;

 hence thesis by A1;

 end;

 suppose

 A8: k <> 0 ;

 A9:

 now

 let m be Nat;

 assume

 A10: m is_at_least_length_of t;

 now

 assume m < (k + 1);

 then

 A11: m <= k by NAT_1: 13;

 (t . k) = ( 1_ L) by A8, Lm10;

 hence contradiction by A10, A11, ALGSEQ_1:def 2;

 end;

 hence (k + 1) <= m;

 end;

 now

 let i be Nat;

 assume i >= (k + 1);

 then i > k by NAT_1: 13;

 hence (t . i) = ( 0. L) by Lm11;

 end;

 then (k + 1) is_at_least_length_of t by ALGSEQ_1:def 2;

 then ( len ( rpoly (k,z))) = (k + 1) by A9, ALGSEQ_1:def 3;

 hence thesis;

 end;

 end;

 theorem :: HURWITZ:28



 Th28: for L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non degenerated non empty doubleLoopStr holds for p be Polynomial of L holds ( deg p) = 1 iff ex x,z be Element of L st x <> ( 0. L) & p = (x * ( rpoly (1,z)))

 proof

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

 A1:

 now

 set x = (p . 1), z = (( - (p . 0 )) * ((p . 1) " ));

 set f = (x * ( rpoly (1,z)));

 assume

 A2: ( deg p) = 1;

 then

 A3: ( len p) = (1 + 1);

 then

 A4: x <> ( 0. L) by ALGSEQ_1: 10;

 A5:

 now

 let k be Nat;

 assume k < ( len p);

 then k < (1 + 1) by A2;

 then

 A6: k <= 1 by NAT_1: 13;

 per cases by A6, XXREAL_0: 1;

 suppose

 A7: k = 1;



 hence (f . k) = (x * (( rpoly (1,z)) . 1)) by POLYNOM5:def 4

 .= (x * ( 1_ L)) by Lm10

 .= (p . k) by A7;

 end;

 suppose k < 1;

 then

 A8: k = 0 by NAT_1: 14;



 hence (f . k) = (x * (( rpoly (1,z)) . 0 )) by POLYNOM5:def 4

 .= (x * ( - (( power L) . (z,(1 + 0 ))))) by Lm10

 .= (x * ( - ((( power L) . (z, 0 )) * z))) by GROUP_1:def 7

 .= (x * ( - (( 1_ L) * z))) by GROUP_1:def 7

 .= (x * ( - z))

 .= ((p . 1) * ( - ( - ((p . 0 ) * ((p . 1) " ))))) by VECTSP_1: 9

 .= ((p . 1) * ((p . 0 ) * ((p . 1) " ))) by RLVECT_1: 17

 .= (((p . 1) * ((p . 1) " )) * (p . 0 )) by GROUP_1:def 3

 .= (( 1_ L) * (p . 0 )) by A4, VECTSP_1:def 10

 .= (p . k) by A8;

 end;

 end;

 ( len f) = (( deg ( rpoly (1,z))) + 1) by A3, ALGSEQ_1: 10, POLYNOM5: 25

 .= (1 + 1) by Th27

 .= ( len p) by A2;

 then p = f by A5, ALGSEQ_1: 12;

 hence ex x,z be Element of L st x <> ( 0. L) & p = (x * ( rpoly (1,z))) by A3, ALGSEQ_1: 10;

 end;

 now

 given x,z be Element of L such that

 A9: x <> ( 0. L) and

 A10: p = (x * ( rpoly (1,z)));



 thus ( deg p) = ( deg ( rpoly (1,z))) by A9, A10, POLYNOM5: 25

 .= 1 by Th27;

 end;

 hence thesis by A1;

 end;

 theorem :: HURWITZ:29



 Th29: for L be add-associative right_zeroed right_complementable Abelian well-unital non degenerated non empty doubleLoopStr holds for x,z be Element of L holds ( eval (( rpoly (1,z)),x)) = (x - z)

 proof



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



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

 let L be add-associative right_zeroed right_complementable Abelian well-unital non degenerated non empty doubleLoopStr, x,z be Element of L;

 set p = ( rpoly (1,z));

 consider F be FinSequence of L such that

 A3: ( eval (p,x)) = ( Sum F) and

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

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



 A6: ( deg p) = 1 by Th27;



 then

 A7: F = <*(F . 1), (F . 2)*> by A4, FINSEQ_1: 44

 .= ( <*(F . 1)*> ^ <*(F . 2)*>);

 2 in ( Seg ( len F)) by A4, A6;

 then 2 in ( dom F) by FINSEQ_1:def 3;



 then

 A8: (F . 2) = ((p . 1) * (( power L) . (x,(1 + 0 )))) by A5, A1

 .= ((p . 1) * ((( power L) . (x, 0 )) * x)) by GROUP_1:def 7

 .= ((p . 1) * (( 1_ L) * x)) by GROUP_1:def 7

 .= ((p . 1) * x)

 .= (( 1_ L) * x) by Lm10

 .= x;

 1 in ( Seg ( len F)) by A4, A6, FINSEQ_1: 2;

 then 1 in ( dom F) by FINSEQ_1:def 3;



 then (F . 1) = ((p . 0 ) * (( power L) . (x,(1 -' 1)))) by A5, A2

 .= ((p . 0 ) * ( 1_ L)) by A2, GROUP_1:def 7

 .= (p . 0 )

 .= ( - (( power L) . (z,(1 + 0 )))) by Lm10

 .= ( - ((( power L) . (z, 0 )) * z)) by GROUP_1:def 7

 .= ( - (( 1_ L) * z)) by GROUP_1:def 7

 .= ( - z);



 hence ( eval (p,x)) = (( Sum <*( - z)*>) + ( Sum <*x*>)) by A3, A7, A8, RLVECT_1: 41

 .= (( Sum <*( - z)*>) + x) by RLVECT_1: 44

 .= (( - z) + x) by RLVECT_1: 44

 .= (x - z) by RLVECT_1:def 11;

 end;

 theorem :: HURWITZ:30



 Th30: for L be add-associative right_zeroed right_complementable well-unital Abelian non degenerated non empty doubleLoopStr holds for z be Element of L holds z is_a_root_of ( rpoly (1,z))

 proof

 let L be Abelian well-unital add-associative right_zeroed non degenerated right_complementable non empty doubleLoopStr, z be Element of L;

 ( eval (( rpoly (1,z)),z)) = (z - z) by Th29

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

 hence thesis by POLYNOM5:def 7;

 end;

 definition

 let L be well-unital non empty doubleLoopStr;

 let z be Element of L;

 let k be Nat;

 :: HURWITZ:def4

 func qpoly (k,z) -> Polynomial of L means

 : Def4: (for i be Nat st i < k holds (it . i) = (( power L) . (z,((k - i) - 1)))) & for i be Nat st i >= k holds (it . i) = ( 0. L);

 existence

 proof

 defpred P[ object, object] means ex n be Element of NAT st n = $1 & (n < k implies $2 = (( power L) . (z,((k - n) - 1)))) & (n >= k implies $2 = ( 0. L));



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

 proof

 let u be object;

 assume u in NAT ;

 then

 reconsider u9 = u as Element of NAT ;

 per cases ;

 suppose

 A2: u9 < k;

 then

 reconsider ku = (k - u9) as Element of NAT by INT_1: 5;

 (k - k) < ku by A2, XREAL_1: 10;

 then ( 0 + 1) < (ku + 1) by XREAL_1: 6;

 then 1 <= (k - u9) by NAT_1: 13;

 then

 reconsider m = ((k - u9) - 1) as Element of NAT by INT_1: 5;

 take (( power L) . (z,((k - u9) - 1)));

 (( power L) . (z,m)) in the carrier of L;

 hence thesis by A2;

 end;

 suppose

 A3: u9 >= k;

 take ( 0. L);

 thus thesis by A3;

 end;

 end;

 consider f be sequence of the carrier of L such that

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

 reconsider f as sequence of L;



 A5: for i be Nat st i >= k holds (f . i) = ( 0. L)

 proof

 let i be Nat;

 i in NAT by ORDINAL1:def 12;

 then

 A6: ex n be Element of NAT st n = i & (n < k implies (f . i) = (( power L) . (z,((k - n) - 1)))) & (n >= k implies (f . i) = ( 0. L)) by A4;

 assume i >= k;

 hence thesis by A6;

 end;

 then

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

 take p;

 now

 let i be Nat;

 i in NAT by ORDINAL1:def 12;

 then

 A7: ex n be Element of NAT st n = i & (n < k implies (f . i) = (( power L) . (z,((k - n) - 1)))) & (n >= k implies (f . i) = ( 0. L)) by A4;

 assume i < k;

 hence (p . i) = (( power L) . (z,((k - i) - 1))) by A7;

 end;

 hence thesis by A5;

 end;

 uniqueness

 proof

 let z1,z2 be AlgSequence of L;

 assume that

 A8: for i be Nat st i < k holds (z1 . i) = (( power L) . (z,((k - i) - 1))) and

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

 assume that

 A10: for i be Nat st i < k holds (z2 . i) = (( power L) . (z,((k - i) - 1))) and

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

 A12:

 now

 let x be object;

 assume x in ( dom z1);

 then

 reconsider x9 = x as Element of NAT ;

 per cases ;

 suppose

 A13: x9 < k;



 hence (z1 . x) = (( power L) . (z,((k - x9) - 1))) by A8

 .= (z2 . x) by A10, A13;

 end;

 suppose

 A14: x9 >= k;



 hence (z1 . x) = ( 0. L) by A9

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

 end;

 end;

 ( dom z1) = NAT by FUNCT_2:def 1

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

 hence z1 = z2 by A12, FUNCT_1: 2;

 end;

 end

 theorem :: HURWITZ:31

 for L be well-unital non degenerated non empty doubleLoopStr holds for z be Element of L holds for k be Element of NAT st k >= 1 holds ( deg ( qpoly (k,z))) = (k - 1)

 proof

 let L be well-unital non degenerated non empty doubleLoopStr;

 let z be Element of L;

 let k be Element of NAT ;

 set p = ( qpoly (k,z));



 A1: (k - 1) < (k - 0 ) by XREAL_1: 10;

 assume k >= 1;

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

 then

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

 ((k - k9) - 1) = 0 ;



 then (p . (k - 1)) = (( power L) . (z, 0 )) by A1, Def4

 .= ( 1_ L) by GROUP_1:def 7;

 then

 A2: (p . (k - 1)) <> ( 0. L);

 A3:

 now

 let m be Nat;

 assume

 A4: m is_at_least_length_of p;

 now

 assume k > m;

 then (k9 + 1) > m;

 then k9 >= m by NAT_1: 13;

 hence contradiction by A2, A4, ALGSEQ_1:def 2;

 end;

 hence k <= m;

 end;

 for i be Nat st i >= k holds (p . i) = ( 0. L) by Def4;

 then k is_at_least_length_of p by ALGSEQ_1:def 2;

 hence thesis by A3, ALGSEQ_1:def 3;

 end;

 theorem :: HURWITZ:32



 Th32: for L be add-associative right_zeroed right_complementable left-distributive well-unital commutative non empty doubleLoopStr holds for z be Element of L holds for k be Element of NAT st k > 1 holds (( rpoly (1,z)) *' ( qpoly (k,z))) = ( rpoly (k,z))

 proof

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

 let z be Element of L, k be Element of NAT ;

 set p = (( rpoly (1,z)) *' ( qpoly (k,z))), u = ( rpoly (k,z));

 assume

 A1: k > 1;

 then

 reconsider k1 = (k - 1) as Element of NAT by INT_1: 5;

 (k1 + 1) = k;

 then

 A2: k1 <= k by INT_1: 6;

 k1 <> k;

 then

 A3: k1 < k by A2, XXREAL_0: 1;

 A4:

 now



 A5: (1 - 1) >= 0 ;

 let i9 be object;



 A6: ( 0 + 1) = 1;

 assume i9 in ( dom p);

 then

 reconsider i = i9 as Element of NAT ;

 consider fp be FinSequence of L such that

 A7: ( len fp) = (i + 1) and

 A8: (p . i) = ( Sum fp) and

 A9: for j be Element of NAT st j in ( dom fp) holds (fp . j) = ((( rpoly (1,z)) . (j -' 1)) * (( qpoly (k,z)) . ((i + 1) -' j))) by POLYNOM3:def 9;



 A10: ((i + 1) - 2) = (i - 1);

 ( len fp) >= 1 by A7, NAT_1: 11;

 then 1 in ( Seg ( len fp));

 then

 A11: 1 in ( dom fp) by FINSEQ_1:def 3;



 then

 A12: (fp /. 1) = (fp . 1) by PARTFUN1:def 6

 .= ((( rpoly (1,z)) . (1 -' 1)) * (( qpoly (k,z)) . ((i + 1) -' 1))) by A9, A11

 .= ((( rpoly (1,z)) . 0 ) * (( qpoly (k,z)) . ((i + 1) -' 1))) by A5, XREAL_0:def 2

 .= (( - (( power L) . (z,1))) * (( qpoly (k,z)) . ((i + 1) -' 1))) by Lm10

 .= (( - ((( power L) . (z, 0 )) * z)) * (( qpoly (k,z)) . ((i + 1) -' 1))) by A6, GROUP_1:def 7

 .= (( - (( 1_ L) * z)) * (( qpoly (k,z)) . ((i + 1) -' 1))) by GROUP_1:def 7

 .= (( - z) * (( qpoly (k,z)) . ((i + 1) -' 1)))

 .= (( - z) * (( qpoly (k,z)) . i)) by NAT_D: 34;

 A13:

 now

 let j be Element of NAT ;

 assume that

 A14: j in ( dom fp) and

 A15: j <> 1 and

 A16: j <> 2;



 A17: j in ( Seg ( len fp)) by A14, FINSEQ_1:def 3;

 now

 assume

 A18: (j -' 1) = 0 or (j -' 1) = 1;

 per cases ;

 suppose (j - 1) >= 0 ;

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

 hence contradiction by A15, A16, A18;

 end;

 suppose (j - 1) < 0 ;

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

 hence contradiction by A17, FINSEQ_1: 1;

 end;

 end;

 then

 A19: (( rpoly (1,z)) . (j -' 1)) = ( 0. L) by Lm11;

 (fp . j) = ((( rpoly (1,z)) . (j -' 1)) * (( qpoly (k,z)) . ((i + 1) -' j))) by A9, A14;

 hence (fp . j) = ( 0. L) by A19;

 end;

 A20:

 now



 A21: (1 + 1) = 2;

 consider g1,g2 be FinSequence of L such that

 A22: ( len g1) = 1 and

 A23: ( len g2) = i and

 A24: fp = (g1 ^ g2) by A7, FINSEQ_2: 23;



 A25: g1 = <*(g1 . 1)*> by A22, FINSEQ_1: 40

 .= <*(fp . 1)*> by A22, A24, FINSEQ_1: 64

 .= <*(fp /. 1)*> by A11, PARTFUN1:def 6;

 assume i <> 0 ;

 then

 A26: (i + 1) > ( 0 + 1) by XREAL_1: 8;

 then

 A27: i >= 1 by NAT_1: 13;

 then 1 in ( Seg ( len g2)) by A23;

 then

 A28: 1 in ( dom g2) by FINSEQ_1:def 3;

 (1 + 1) <= ( len fp) by A7, A26, NAT_1: 13;

 then 2 in ( Seg ( len fp));

 then

 A29: 2 in ( dom fp) by FINSEQ_1:def 3;

 now

 let i be Element of NAT ;

 assume that

 A30: i in ( dom g2) and

 A31: i <> 1;



 A32: (i + 1) <> 2 by A31;



 A33: 1 <= (i + 1) by NAT_1: 11;



 A34: i in ( Seg ( len g2)) by A30, FINSEQ_1:def 3;

 then

 A35: i <= ( len g2) by FINSEQ_1: 1;

 ( len fp) = (1 + ( len g2)) by A22, A24, FINSEQ_1: 22;

 then (i + 1) <= ( len fp) by A35, XREAL_1: 6;

 then (i + 1) in ( Seg ( len fp)) by A33;

 then

 A36: (i + 1) in ( dom fp) by FINSEQ_1:def 3;

 (i + 1) <> ( 0 + 1) by A34, FINSEQ_1: 1;

 then

 A37: (fp . (i + 1)) = ( 0. L) by A13, A36, A32;

 1 <= i by A34, FINSEQ_1: 1;

 then (g2 . i) = (fp . (i + 1)) by A22, A24, A35, FINSEQ_1: 65;

 hence (g2 /. i) = ( 0. L) by A30, A37, PARTFUN1:def 6;

 end;



 then ( Sum g2) = (g2 /. 1) by A28, POLYNOM2: 3

 .= (g2 . 1) by A28, PARTFUN1:def 6

 .= (fp . 2) by A27, A22, A23, A24, A21, FINSEQ_1: 65

 .= (fp /. 2) by A29, PARTFUN1:def 6;



 hence (p . i) = (( Sum g1) + (fp /. 2)) by A8, A24, RLVECT_1: 41

 .= ((fp /. 1) + (fp /. 2)) by A25, RLVECT_1: 44;

 end;



 A38: (2 - 1) >= 0 ;

 A39:

 now

 assume i <> 0 ;

 then

 A40: (i + 1) > ( 0 + 1) by XREAL_1: 8;

 then i >= 1 by NAT_1: 13;

 then

 reconsider i1 = (i - 1) as Element of NAT by INT_1: 5;

 ( len fp) >= (1 + 1) by A7, A40, NAT_1: 13;

 then 2 in ( Seg ( len fp));

 then

 A41: 2 in ( dom fp) by FINSEQ_1:def 3;



 then

 A42: (fp . 2) = ((( rpoly (1,z)) . (2 -' 1)) * (( qpoly (k,z)) . ((i + 1) -' 2))) by A9

 .= ((( rpoly (1,z)) . 1) * (( qpoly (k,z)) . ((i + 1) -' 2))) by A38, XREAL_0:def 2

 .= (( 1_ L) * (( qpoly (k,z)) . ((i + 1) -' 2))) by Lm10

 .= (( qpoly (k,z)) . ((i + 1) -' 2))

 .= (( qpoly (k,z)) . i1) by A10, XREAL_0:def 2;



 thus (fp /. 2) = (fp . 2) by A41, PARTFUN1:def 6

 .= (( qpoly (k,z)) . (i -' 1)) by A42, XREAL_0:def 2;

 end;

 per cases by XXREAL_0: 1;

 suppose

 A43: i < k;

 per cases ;

 suppose

 A44: i = 0 ;



 A45: ((k - 0 ) - 1) = k1;



 A46: (k1 + 1) = k;

 fp = <*(fp . 1)*> by A7, A44, FINSEQ_1: 40

 .= <*(fp /. 1)*> by A11, PARTFUN1:def 6;



 hence (p . i9) = (( - z) * (( qpoly (k,z)) . 0 )) by A8, A12, A44, RLVECT_1: 44

 .= (( - z) * (( power L) . (z,k1))) by A45, A46, Def4

 .= ( - (z * (( power L) . (z,k1)))) by VECTSP_1: 9

 .= ( - (( power L) . (z,k))) by A46, GROUP_1:def 7

 .= (u . i9) by A1, A44, Lm10;

 end;

 suppose

 A47: i > 0 ;

 then (i + 1) > ( 0 + 1) by XREAL_1: 6;

 then i >= 1 by NAT_1: 13;

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

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

 then

 A48: ((k - (i -' 1)) - 1) = (k - i);

 (k - i) > (i - i) by A43, XREAL_1: 9;

 then

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

 ki > (i - i) by A43, XREAL_1: 9;

 then (ki + 1) > ( 0 + 1) by XREAL_1: 6;

 then ki >= 1 by NAT_1: 13;

 then

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



 A49: (k - 1) < (k - 0 ) by XREAL_1: 10;

 (i - 1) < (k - 1) by A43, XREAL_1: 9;

 then

 A50: (i - 1) < k by A49, XXREAL_0: 2;



 A51: (ki1 + 1) = ki;



 thus (p . i9) = ((( - z) * (( power L) . (z,ki1))) + (( qpoly (k,z)) . (i -' 1))) by A12, A39, A20, A43, A47, Def4

 .= ((( - z) * (( power L) . (z,ki1))) + (( power L) . (z,ki))) by A48, A50, Def4

 .= (( - (z * (( power L) . (z,ki1)))) + (( power L) . (z,ki))) by VECTSP_1: 9

 .= (( - (( power L) . (z,ki))) + (( power L) . (z,ki))) by A51, GROUP_1:def 7

 .= ( 0. L) by RLVECT_1: 5

 .= (u . i9) by A43, A47, Lm11;

 end;

 end;

 suppose

 A52: i = k;

 then (i - 1) >= (1 - 1) by A1, XREAL_1: 9;

 then

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



 A54: ((k - k1) - 1) = 0 ;

 (fp /. 1) = (( - z) * ( 0. L)) by A12, A52, Def4

 .= ( 0. L);



 hence (p . i9) = (( qpoly (k,z)) . k1) by A39, A20, A52, A53, ALGSTR_1:def 2

 .= (( power L) . (z, 0 )) by A3, A54, Def4

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

 .= (u . i9) by A1, A52, Lm10;

 end;

 suppose

 A55: i > k;

 then (i + 1) > ( 0 + 1) by XREAL_1: 6;

 then i >= 1 by NAT_1: 13;

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

 then

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

 i >= (k + 1) by A55, NAT_1: 13;

 then

 A57: (i - 1) >= ((k + 1) - 1) by XREAL_1: 9;

 (fp /. 1) = (( - z) * ( 0. L)) by A12, A55, Def4

 .= ( 0. L);



 hence (p . i9) = (( qpoly (k,z)) . (i -' 1)) by A39, A20, A55, ALGSTR_1:def 2

 .= ( 0. L) by A56, A57, Def4

 .= (u . i9) by A55, Lm11;

 end;

 end;

 ( dom p) = NAT by FUNCT_2:def 1

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

 hence thesis by A4, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:33



 Th33: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative non empty doubleLoopStr holds for p be Polynomial of L holds for z be Element of L st z is_a_root_of p holds ex s be Polynomial of L st p = (( rpoly (1,z)) *' s)

 proof

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

 let p be Polynomial of L;

 let z be Element of L;

 assume

 A1: z is_a_root_of p;

 set m = ( len p);

 per cases ;

 suppose

 A2: m = 0 ;

 take ( 0_. L);

 p = ( 0_. L) by A2, POLYNOM4: 5;

 hence thesis by POLYNOM3: 34;

 end;

 suppose

 A3: m > 0 ;

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

 then

 reconsider m1 = (m - 1) as Element of NAT by INT_1: 5;

 defpred Pr[ set, set] means ex u be Element of L st ex b be Element of NAT st u = (p . $1) & b = $1 & $2 = (u * ( rpoly (b,z)));

 defpred Pq[ set, set] means ($1 = 1 & $2 = ((p . 1) * ( 1_. L))) or ($1 <> 1 & ex u be Element of L st ex b be Element of NAT st u = (p . $1) & b = $1 & $2 = (u * ( qpoly (b,z))));



 A4: for k be Nat st k in ( Seg m1) holds ex x be Element of the carrier of ( Polynom-Ring L) st Pq[k, x]

 proof

 let k be Nat;



 A5: ( dom p) = NAT by FUNCT_2:def 1;

 assume k in ( Seg m1);

 then

 A6: 1 <= k by FINSEQ_1: 1;

 per cases by A6, XXREAL_0: 1;

 suppose

 A7: k = 1;

 reconsider t = ((p . 1) * ( 1_. L)) as Element of the carrier of ( Polynom-Ring L) by POLYNOM3:def 10;

 take t;

 thus thesis by A7;

 end;

 suppose

 A8: k > 1;

 reconsider t = ((p /. k) * ( qpoly (k,z))) as Element of the carrier of ( Polynom-Ring L) by POLYNOM3:def 10;

 take t;

 ex u be Element of L st ex b be Element of NAT st u = (p . k) & b = k & t = (u * ( qpoly (b,z)))

 proof

 take (p /. k);

 reconsider b = k as Element of NAT by ORDINAL1:def 12;

 take b;

 b in NAT ;

 hence thesis by A5, PARTFUN1:def 6;

 end;

 hence thesis by A8;

 end;

 end;

 consider hs be FinSequence of ( Polynom-Ring L) such that

 A9: ( dom hs) = ( Seg m1) & for k be Nat st k in ( Seg m1) holds Pq[k, (hs . k)] from FINSEQ_1:sch 5( A4);

 A10:

 now

 let i be Element of NAT ;

 assume that

 A11: 1 < i and

 A12: i <= (m - 1);

 i in ( Seg m1) by A11, A12;

 then ex u be Element of L st ex b be Element of NAT st u = (p . i) & b = i & (hs . i) = (u * ( qpoly (b,z))) by A9, A11;

 hence (hs . i) = ((p . i) * ( qpoly (i,z)));

 end;



 A13: for k be Nat st k in ( Seg m1) holds ex x be Element of the carrier of ( Polynom-Ring L) st Pr[k, x]

 proof

 let k be Nat;

 assume k in ( Seg m1);

 then

 reconsider k1 = k as Element of NAT ;

 reconsider t = ((p /. k) * ( rpoly (k1,z))) as Element of the carrier of ( Polynom-Ring L) by POLYNOM3:def 10;

 take t;

 take (p /. k);

 take k1;



 A14: k1 in NAT ;

 ( dom p) = NAT by FUNCT_2:def 1;

 hence thesis by A14, PARTFUN1:def 6;

 end;

 consider h be FinSequence of ( Polynom-Ring L) such that

 A15: ( dom h) = ( Seg m1) & for k be Nat st k in ( Seg m1) holds Pr[k, (h . k)] from FINSEQ_1:sch 5( A13);

 set s = ( Sum hs), rs = ( Sum h);

 reconsider s, rs as Polynomial of L by POLYNOM3:def 10;

 A16:

 now

 let k be Element of NAT ;

 assume that

 A17: 1 <= k and

 A18: k <= m1;

 k in ( Seg m1) by A17, A18;

 then ex u be Element of L st ex b be Element of NAT st u = (p . k) & b = k & (h . k) = (u * ( rpoly (b,z))) by A15;

 hence (h . k) = ((p . k) * ( rpoly (k,z)));

 end;



 A19: (m1 + 1) = m;

 A20:

 now

 let i be Element of NAT ;

 assume

 A21: i >= ( len p);

 set co = ( Coeff (h,i));



 A22: ( dom h) = ( Seg ( len h)) by FINSEQ_1:def 3

 .= ( Seg ( len co)) by Def1

 .= ( dom co) by FINSEQ_1:def 3;

 now

 let j be Element of NAT ;

 assume

 A23: j in ( dom co);

 then

 A24: ex ci be Polynomial of L st ci = (h . j) & (co . j) = (ci . i) by Def1;



 A25: j <= m1 by A15, A22, A23, FINSEQ_1: 1;

 then

 A26: j <> i by A19, A21, NAT_1: 16, XXREAL_0: 2;

 1 <= j by A15, A22, A23, FINSEQ_1: 1;



 hence (co . j) = (((p . j) * ( rpoly (j,z))) . i) by A16, A24, A25

 .= ((p . j) * (( rpoly (j,z)) . i)) by POLYNOM5:def 4

 .= ((p . j) * ( 0. L)) by A3, A21, A26, Lm11

 .= ( 0. L);

 end;

 then ( Sum co) = ( 0. L) by POLYNOM3: 1;

 hence (rs . i) = ( 0. L) by Th13;

 end;



 A27: ( len h) = m1 by A15, FINSEQ_1:def 3;

 A28:

 now

 let i be Element of NAT ;

 assume that

 A29: i > 0 and

 A30: i < ( len p);

 i < (m1 + 1) by A30;

 then

 A31: i <= m1 by NAT_1: 13;

 (i + 1) > ( 0 + 1) by A29, XREAL_1: 8;

 then

 A32: i >= 1 by NAT_1: 13;

 then

 A33: (h . i) = ((p . i) * ( rpoly (i,z))) by A16, A31;

 set co = ( Coeff (h,i));



 A34: ( dom h) = ( Seg ( len h)) by FINSEQ_1:def 3

 .= ( Seg ( len co)) by Def1

 .= ( dom co) by FINSEQ_1:def 3;

 i in ( Seg ( len h)) by A27, A32, A31;

 then

 A35: i in ( dom co) by A34, FINSEQ_1:def 3;

 then

 A36: ex cc be Polynomial of L st cc = (h . i) & (co . i) = (cc . i) by Def1;

 now

 let i9 be Element of NAT ;

 assume that

 A37: i9 in ( dom co) and

 A38: i9 <> i;



 A39: ex ci be Polynomial of L st ci = (h . i9) & (co . i9) = (ci . i) by A37, Def1;



 A40: i9 <= (m - 1) by A15, A34, A37, FINSEQ_1: 1;

 1 <= i9 by A15, A34, A37, FINSEQ_1: 1;



 then (co . i9) = (((p . i9) * ( rpoly (i9,z))) . i) by A16, A39, A40

 .= ((p . i9) * (( rpoly (i9,z)) . i)) by POLYNOM5:def 4

 .= ((p . i9) * ( 0. L)) by A29, A38, Lm11

 .= ( 0. L);

 hence (co /. i9) = ( 0. L) by A37, PARTFUN1:def 6;

 end;



 then ( Sum co) = (co /. i) by A35, POLYNOM2: 3

 .= (co . i) by A35, PARTFUN1:def 6;

 hence (rs . i) = (((p . i) * ( rpoly (i,z))) . i) by A36, A33, Th13;

 end;

 A41:

 now

 let i9 be object;

 assume i9 in ( dom p);

 then

 reconsider i = i9 as Element of NAT ;

 per cases ;

 suppose

 A42: i = 0 ;

 set co = ( Coeff (h, 0 ));

 consider evp be FinSequence of L such that

 A43: ( eval (p,z)) = ( Sum evp) and

 A44: ( len evp) = ( len p) and

 A45: for n be Element of NAT st n in ( dom evp) holds (evp . n) = ((p . (n -' 1)) * (( power L) . (z,(n -' 1)))) by POLYNOM4:def 2;

 set cop = ( <*( - (p . 0 ))*> ^ co);



 A46: ( len cop) = (( len <*( - (p . 0 ))*>) + ( len co)) by FINSEQ_1: 22

 .= (1 + ( len co)) by FINSEQ_1: 39;



 then

 A47: ( len cop) = (1 + ( len h)) by Def1

 .= ( len evp) by A27, A44;



 then

 A48: ( dom cop) = ( Seg ( len evp)) by FINSEQ_1:def 3

 .= ( dom evp) by FINSEQ_1:def 3;



 A49: ( dom h) = ( Seg ( len h)) by FINSEQ_1:def 3

 .= ( Seg ( len co)) by Def1

 .= ( dom co) by FINSEQ_1:def 3;

 A50:

 now

 let j be Element of NAT ;

 reconsider aj = ( - (( power L) . (z,j))) as Element of L;

 assume

 A51: j in ( dom co);

 then

 A52: 1 <= j by A15, A49, FINSEQ_1: 1;



 A53: j <= m1 by A15, A49, A51, FINSEQ_1: 1;

 ex ci be Polynomial of L st ci = (h . j) & (co . j) = (ci . i) by A42, A51, Def1;



 hence (co . j) = (((p . j) * ( rpoly (j,z))) . i) by A16, A52, A53

 .= ((p . j) * (( rpoly (j,z)) . i)) by POLYNOM5:def 4

 .= ((p . j) * aj) by A42, A52, Lm10

 .= ( - ((p . j) * (( power L) . (z,j)))) by VECTSP_1: 8;

 end;

 now

 let j be Element of NAT ;



 A54: ( dom <*( - (p . 0 ))*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

 assume

 A55: j in ( dom cop);



 then

 A56: (evp /. j) = (evp . j) by A48, PARTFUN1:def 6

 .= ((p . (j -' 1)) * (( power L) . (z,(j -' 1)))) by A45, A48, A55;



 A57: j in ( Seg ( len cop)) by A55, FINSEQ_1:def 3;

 then

 A58: 1 <= j by FINSEQ_1: 1;



 A59: j <= ( len cop) by A57, FINSEQ_1: 1;

 per cases by A58, XXREAL_0: 1;

 suppose

 A60: j = 1;

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



 then

 A61: (evp /. j) = ((p . 0 ) * ( 1_ L)) by A56, GROUP_1:def 7

 .= (p . 0 );

 j in ( dom <*( - (p . 0 ))*>) by A54, A60, TARSKI:def 1;



 then (cop . j) = ( <*( - (p . 0 ))*> . j) by FINSEQ_1:def 7

 .= ( - (p . 0 )) by A60, FINSEQ_1: 40;

 hence (cop /. j) = ( - (evp /. j)) by A55, A61, PARTFUN1:def 6;

 end;

 suppose

 A62: j > 1;

 then

 reconsider j1 = (j - 1) as Element of NAT by INT_1: 5;

 1 < (j1 + 1) by A62;

 then

 A63: 1 <= j1 by NAT_1: 13;

 j1 <= (( len cop) - 1) by A59, XREAL_1: 9;

 then j1 in ( Seg ( len co)) by A46, A63;

 then

 A64: j1 in ( dom co) by FINSEQ_1:def 3;



 A65: j <= ( len cop) by A57, FINSEQ_1: 1;

 (j - 1) >= (1 - 1) by A62, XREAL_1: 9;

 then

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

 ( len <*( - (p . 0 ))*>) < j by A62, FINSEQ_1: 40;



 then (cop . j) = (co . (j - ( len <*( - (p . 0 ))*>))) by A65, FINSEQ_1: 24

 .= (co . (j - 1)) by FINSEQ_1: 40

 .= ( - ((p . j1) * (( power L) . (z,j1)))) by A50, A64;

 hence (cop /. j) = ( - (evp /. j)) by A55, A56, A66, PARTFUN1:def 6;

 end;

 end;



 then

 A67: ( - ( Sum evp)) = ( Sum cop) by A47, Th7

 .= (( Sum <*( - (p . 0 ))*>) + ( Sum co)) by RLVECT_1: 41

 .= (( - (p . 0 )) + ( Sum co)) by RLVECT_1: 44;

 ( Sum evp) = ( 0. L) by A1, A43, POLYNOM5:def 7;

 then ( 0. L) = (( - (p . 0 )) + ( Sum co)) by A67, RLVECT_1: 12;



 then (p . 0 ) = ((p . 0 ) + (( - (p . 0 )) + ( Sum co))) by ALGSTR_1:def 2

 .= (((p . 0 ) + ( - (p . 0 ))) + ( Sum co)) by RLVECT_1:def 3

 .= (( 0. L) + ( Sum co)) by RLVECT_1: 5

 .= ( Sum co) by ALGSTR_1:def 2;

 hence (p . i9) = (rs . i9) by A42, Th13;

 end;

 suppose

 A68: i > 0 ;

 per cases ;

 suppose

 A69: i >= ( len p);



 hence (rs . i9) = ( 0. L) by A20

 .= (p . i9) by A69, ALGSEQ_1: 8;

 end;

 suppose i < ( len p);



 hence (rs . i9) = (((p . i) * ( rpoly (i,z))) . i) by A28, A68

 .= ((p . i) * (( rpoly (i,z)) . i)) by POLYNOM5:def 4

 .= ((p . i) * ( 1_ L)) by A68, Lm10

 .= (p . i9);

 end;

 end;

 end;

 now

 assume m1 < 1;

 then ( deg p) = 0 by NAT_1: 14;

 then not p is with_roots by Th24;

 hence contradiction by A1, POLYNOM5:def 8;

 end;

 then 1 in ( Seg m1);

 then

 A70: (hs . 1) = ((p . 1) * ( 1_. L)) by A9;

 A71:

 now

 reconsider r1z = ( rpoly (1,z)) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

 let i9 be object;

 assume i9 in ( dom rs);



 A72: ( dom (r1z * hs)) = ( dom h) by A9, A15, POLYNOM1:def 1;

 now

 let k be Nat;

 assume

 A73: k in ( dom h);

 then

 A74: 1 <= k by A15, FINSEQ_1: 1;



 A75: k <= m1 by A15, A73, FINSEQ_1: 1;

 per cases by A74, XXREAL_0: 1;

 suppose

 A76: k = 1;

 then

 A77: (hs /. k) = ((p . 1) * ( 1_. L)) by A9, A70, A15, A73, PARTFUN1:def 6;



 thus ((r1z * hs) . k) = ((r1z * hs) /. k) by A72, A73, PARTFUN1:def 6

 .= (r1z * (hs /. k)) by A9, A15, A73, POLYNOM1:def 1

 .= (( rpoly (1,z)) *' ((p . 1) * ( 1_. L))) by A77, POLYNOM3:def 10

 .= ((p . 1) * (( rpoly (1,z)) *' ( 1_. L))) by Th19

 .= ((p . 1) * ( rpoly (1,z))) by POLYNOM3: 35

 .= (h . k) by A16, A75, A76;

 end;

 suppose

 A78: k > 1;

 reconsider k1 = k as Element of NAT by A73;



 A79: (hs /. k) = (hs . k) by A9, A15, A73, PARTFUN1:def 6

 .= ((p . k1) * ( qpoly (k1,z))) by A10, A75, A78;



 thus ((r1z * hs) . k) = ((r1z * hs) /. k) by A72, A73, PARTFUN1:def 6

 .= (r1z * (hs /. k)) by A9, A15, A73, POLYNOM1:def 1

 .= (( rpoly (1,z)) *' ((p . k1) * ( qpoly (k1,z)))) by A79, POLYNOM3:def 10

 .= ((p . k1) * (( rpoly (1,z)) *' ( qpoly (k1,z)))) by Th19

 .= ((p . k1) * ( rpoly (k1,z))) by A78, Th32

 .= (h . k) by A16, A74, A75;

 end;

 end;

 then (r1z * hs) = h by A72, FINSEQ_1: 13;

 hence (rs . i9) = ((( rpoly (1,z)) *' s) . i9) by Lm5;

 end;

 take s;

 ( dom (( rpoly (1,z)) *' s)) = NAT by FUNCT_2:def 1

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

 then

 A80: (( rpoly (1,z)) *' s) = rs by A71, FUNCT_1: 2;

 ( dom p) = NAT by FUNCT_2:def 1

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

 hence thesis by A80, A41, FUNCT_1: 2;

 end;

 end;

 begin

 definition

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

 let p,s be Polynomial of L;

 :: HURWITZ:def5

 func p div s -> Polynomial of L means

 : Def5: ex t be Polynomial of L st p = ((it *' s) + t) & ( deg t) < ( deg s);

 existence

 proof

 set M = { (p - (u *' s)) where u be Polynomial of L : 1 = 1 };

 defpred P[ Nat] means ex t be Polynomial of L st t in M & ( len t) = $1;



 A2: ( len s) <> 0 by A1, POLYNOM4: 5;

 then (( len s) + 1) > ( 0 + 1) by XREAL_1: 6;

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

 then

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

 (s . (( len s) - 1)) <> ( 0. L) by A2, Lm6;

 then

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

 p = (p + ( 0_. L)) by POLYNOM3: 28

 .= (p + ( - ( 0_. L))) by Th9

 .= (p - (( 0_. L) *' s)) by POLYNOM4: 2;

 then p in M;

 then ex t be Polynomial of L st t in M & ( len t) = ( len p);

 then

 A5: ex k be Nat st P[k];

 consider k be Nat such that

 A6: P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A5);

 consider f be Polynomial of L such that

 A7: f in M and

 A8: ( len f) = k by A6;

 consider g be Polynomial of L such that

 A9: f = (p - (g *' s)) and 1 = 1 by A7;

 take g;



 A10: ((g *' s) + (p - (g *' s))) = (((g *' s) + ( - (g *' s))) + p) by POLYNOM3: 26

 .= (((g *' s) - (g *' s)) + p)

 .= (( 0_. L) + p) by POLYNOM3: 29

 .= p by POLYNOM3: 28;

 per cases ;

 suppose

 A11: f = ( 0_. L);

 reconsider s9 = ( deg s) as Nat by A1, Lm8;



 A12: s9 >= 0 ;

 ( deg f) = ( - 1) by A11, Th20;

 hence thesis by A9, A10, A12;

 end;

 suppose f <> ( 0_. L);

 then ( len f) <> 0 by POLYNOM4: 5;

 then (( len f) + 1) > ( 0 + 1) by XREAL_1: 6;

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

 then

 A13: (( len f) - 1) >= (1 - 1) by XREAL_1: 9;

 then

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



 A14: k = (k9 + 1) by A8;

 ( dom f) = NAT by FUNCT_2:def 1;

 then

 A15: k9 in ( dom f);

 now

 assume ( deg f) >= ( deg s);

 then

 reconsider degn = (( deg f) - ( deg s)) as Element of NAT by INT_1: 5;

 set al = ((f . (( len f) -' 1)) * ((s . (( len s) -' 1)) " ));

 set g1 = (( 0_. L) +* ( {degn} --> al));

 now

 let u be object;

 assume u in {degn};

 then u = degn by TARSKI:def 1;

 hence u in NAT ;

 end;

 then

 A17: {degn} c= NAT by TARSKI:def 3;



 A18: degn in {degn} by TARSKI:def 1;

 A19:

 now

 let x9 be object;

 assume x9 in NAT ;

 then

 reconsider x = x9 as Element of NAT ;

 per cases ;

 suppose

 A20: x in ( dom ( {degn} --> al));

 then x = degn by TARSKI:def 1;



 then (g1 . x) = (( {degn} --> al) . degn) by A20, FUNCT_4: 13

 .= al by A18, FUNCOP_1: 7;

 hence (g1 . x9) in the carrier of L;

 end;

 suppose not x in ( dom ( {degn} --> al));



 then (g1 . x) = (( 0_. L) . x) by FUNCT_4: 11

 .= ( 0. L);

 hence (g1 . x9) in the carrier of L;

 end;

 end;

 (( dom ( 0_. L)) \/ ( dom ( {degn} --> al))) = NAT by A17, XBOOLE_1: 12;

 then ( dom g1) = NAT by FUNCT_4:def 1;

 then

 reconsider g1 as sequence of L by A19, FUNCT_2: 3;



 A21: for j be Nat st j <> degn holds (g1 . j) = ( 0. L)

 proof

 let j be Nat;



 A22: j in NAT by ORDINAL1:def 12;

 assume j <> degn;

 then not j in ( dom ( {degn} --> al)) by TARSKI:def 1;



 hence (g1 . j) = (( 0_. L) . j) by FUNCT_4: 11

 .= ( 0. L) by A22, FUNCOP_1: 7;

 end;



 A23: ex l be Nat st for i be Nat st i >= l holds (g1 . i) = ( 0. L)

 proof

 take l = (degn + 1);

 now

 let i be Nat;

 assume i >= l;

 then i <> degn by NAT_1: 13;

 hence (g1 . i) = ( 0. L) by A21;

 end;

 hence thesis;

 end;



 A24: degn in {degn} by TARSKI:def 1;

 then degn in ( dom ( {degn} --> al));



 then

 A25: (g1 . degn) = (( {degn} --> al) . degn) by FUNCT_4: 13

 .= al by A24, FUNCOP_1: 7;

 reconsider g1 as Polynomial of L by A23, ALGSEQ_1:def 1;

 set s1 = (p - ((g + g1) *' s));

 now



 A26: 1 <= (degn + 1) by NAT_1: 11;

 let i be Nat;



 A27: ( dom f) = NAT by FUNCT_2:def 1;

 assume

 A28: i >= k9;

 then

 A29: (i + 1) >= k by A14, XREAL_1: 6;

 (degn + 1) = (k - ( deg s)) by A8;

 then

 A30: (degn + 1) <= k by A3, XREAL_1: 43;

 then

 A31: ((i + 1) - (degn + 1)) is Element of NAT by A29, INT_1: 5, XXREAL_0: 2;



 A32: i in NAT by ORDINAL1:def 12;

 then

 consider sf be FinSequence of L such that

 A33: ( len sf) = (i + 1) and

 A34: ((g1 *' s) . i) = ( Sum sf) and

 A35: for m be Element of NAT st m in ( dom sf) holds (sf . m) = ((g1 . (m -' 1)) * (s . ((i + 1) -' m))) by POLYNOM3:def 9;



 A36: ( dom sf) = ( Seg ( len sf)) by FINSEQ_1:def 3;

 (i + 1) >= (degn + 1) by A30, A29, XXREAL_0: 2;

 then

 A37: (degn + 1) in ( dom sf) by A33, A36, A26;

 A38:

 now

 let m be Nat;

 assume that

 A39: m in ( dom sf) and

 A40: m <> (degn + 1);

 1 <= m by A36, A39, FINSEQ_1: 1;

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

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

 then (m -' 1) <> degn by A40;

 hence (g1 . (m -' 1)) = ( 0. L) by A21;

 end;

 now

 let i9 be Element of NAT ;

 assume that

 A41: i9 in ( dom sf) and

 A42: i9 <> (degn + 1);

 (sf . i9) = ((g1 . (i9 -' 1)) * (s . ((i + 1) -' i9))) by A35, A41

 .= (( 0. L) * (s . ((i + 1) -' i9))) by A38, A41, A42

 .= ( 0. L);

 hence (sf /. i9) = ( 0. L) by A41, PARTFUN1:def 6;

 end;



 then

 A43: ( Sum sf) = (sf /. (degn + 1)) by A37, POLYNOM2: 3

 .= (sf . (degn + 1)) by A37, PARTFUN1:def 6

 .= ((g1 . ((degn + 1) -' 1)) * (s . ((i + 1) -' (degn + 1)))) by A35, A37

 .= (al * (s . ((i + 1) -' (degn + 1)))) by A25, NAT_D: 34;



 A44: (s1 - f) = ((p + ( - ((g + g1) *' s))) + (( - p) + ( - ( - (g *' s))))) by A9, Th11

 .= (((p + ( - ((g + g1) *' s))) + ( - p)) + ( - ( - (g *' s)))) by POLYNOM3: 26

 .= (((p - p) + ( - ((g + g1) *' s))) + ( - ( - (g *' s)))) by POLYNOM3: 26

 .= ((( 0_. L) + ( - ((g + g1) *' s))) + ( - ( - (g *' s)))) by POLYNOM3: 29

 .= (( - ((g + g1) *' s)) + ( - ( - (g *' s)))) by POLYNOM3: 28

 .= ((( - (g + g1)) *' s) + ( - ( - (g *' s)))) by Th12

 .= (((( - g) + ( - g1)) *' s) + ( - ( - (g *' s)))) by Th11

 .= (((( - g) + ( - g1)) *' s) + (g *' s)) by Lm3

 .= (((( - g) *' s) + (( - g1) *' s)) + (g *' s)) by POLYNOM3: 32

 .= ((( - g1) *' s) + ((( - g) *' s) + (g *' s))) by POLYNOM3: 26

 .= ((( - g1) *' s) + ((g *' s) - (g *' s))) by Th12

 .= ((( - g1) *' s) + ( 0_. L)) by POLYNOM3: 29

 .= (( - g1) *' s) by POLYNOM3: 28

 .= ( - (g1 *' s)) by Th12;



 A45: ( dom (g1 *' s)) = NAT by FUNCT_2:def 1;

 s1 = (s1 + ( 0_. L)) by POLYNOM3: 28

 .= (s1 + (f - f)) by POLYNOM3: 29

 .= ((s1 + ( - f)) + f) by POLYNOM3: 26

 .= (f - (g1 *' s)) by A44;



 then

 A46: (s1 . i) = ((f . i) + (( - (g1 *' s)) . i)) by NORMSP_1:def 2

 .= ((f . i) + ( - ((g1 *' s) . i))) by BHSP_1: 44

 .= ((f /. i) + ( - ((g1 *' s) . i))) by A32, A27, PARTFUN1:def 6

 .= ((f /. i) + ( - ((g1 *' s) /. i))) by A32, A45, PARTFUN1:def 6;



 A47: i in NAT by ORDINAL1:def 12;

 per cases by A28, XXREAL_0: 1;

 suppose

 A48: i > k9;

 then

 reconsider e = (i - k9) as Element of NAT by INT_1: 5;

 (i - k9) > (k9 - k9) by A48, XREAL_1: 9;

 then (e + 1) > ( 0 + 1) by XREAL_1: 6;

 then e >= 1 by NAT_1: 13;

 then ((i - k9) - 1) >= (1 - 1) by XREAL_1: 9;

 then

 A49: (((i - k9) - 1) + ( len s)) >= ( 0 + ( len s)) by XREAL_1: 6;

 (i + 1) > (k9 + 1) by A48, XREAL_1: 6;

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

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

 then

 A50: (f /. i) = ( 0. L) by A27, A47, PARTFUN1:def 6;

 ((i + 1) -' (degn + 1)) = ((i - k9) + (( len s) - 1)) by A31, XREAL_0:def 2;

 then (s . ((i + 1) -' (degn + 1))) = ( 0. L) by A49, ALGSEQ_1: 8;

 then ( Sum sf) = ( 0. L) by A43;



 hence (s1 . i) = (( 0. L) + ( - ( 0. L))) by A45, A46, A34, A47, A50, PARTFUN1:def 6

 .= (( 0. L) + ( 0. L)) by RLVECT_1: 12

 .= ( 0. L) by RLVECT_1:def 4;

 end;

 suppose

 A51: i = k9;

 ((i + 1) -' (degn + 1)) = ((i + 1) - (degn + 1)) by A31, XREAL_0:def 2

 .= (( len s) -' 1) by A3, A51, XREAL_0:def 2;



 then ( Sum sf) = ((f . (( len f) -' 1)) * (((s . (( len s) -' 1)) " ) * (s . (( len s) -' 1)))) by A43, GROUP_1:def 3

 .= ((f . (( len f) -' 1)) * ( 1_ L)) by A4, VECTSP_1:def 10

 .= (f . (( len f) -' 1))

 .= (f . (( len f) - 1)) by A13, XREAL_0:def 2

 .= (f /. (( len f) - 1)) by A15, PARTFUN1:def 6;



 hence (s1 . i) = ((f /. (( len f) - 1)) + ( - (f /. (( len f) - 1)))) by A45, A46, A34, A51, PARTFUN1:def 6

 .= ( 0. L) by RLVECT_1: 5;

 end;

 end;

 then k9 is_at_least_length_of s1 by ALGSEQ_1:def 2;

 then ( len s1) <= k9 by ALGSEQ_1:def 3;

 then

 A52: ( len s1) < k by A14, NAT_1: 13;

 s1 in M;

 hence contradiction by A6, A52;

 end;

 hence thesis by A9, A10;

 end;

 end;

 uniqueness

 proof

 let f1,f2 be Polynomial of L;

 given t1 be Polynomial of L such that

 A53: p = ((f1 *' s) + t1) and

 A54: ( deg t1) < ( deg s);

 given t2 be Polynomial of L such that

 A55: p = ((f2 *' s) + t2) and

 A56: ( deg t2) < ( deg s);



 A57: ((f2 - f1) *' s) = ((f2 *' s) + (( - f1) *' s)) by POLYNOM3: 32

 .= ((f2 *' s) - (f1 *' s)) by Th12;

 (f2 *' s) = ((f2 *' s) + ( 0_. L)) by POLYNOM3: 28

 .= ((f2 *' s) + (t2 - t2)) by POLYNOM3: 29

 .= (((f1 *' s) + t1) + ( - t2)) by A53, A55, POLYNOM3: 26;



 then

 A58: ((f2 *' s) - (f1 *' s)) = (((f1 *' s) + (t1 + ( - t2))) + ( - (f1 *' s))) by POLYNOM3: 26

 .= ((t1 + ( - t2)) + ((f1 *' s) - (f1 *' s))) by POLYNOM3: 26

 .= ((t1 + ( - t2)) + ( 0_. L)) by POLYNOM3: 29

 .= (t1 - t2) by POLYNOM3: 28;

 now

 assume

 A59: f1 <> f2;

 A60:

 now

 assume (f2 - f1) = ( 0_. L);



 then f1 = ((f2 + ( - f1)) + f1) by POLYNOM3: 28

 .= (f2 + (f1 - f1)) by POLYNOM3: 26

 .= (f2 + ( 0_. L)) by POLYNOM3: 29;

 hence contradiction by A59, POLYNOM3: 28;

 end;

 then

 reconsider d = ( deg (f2 - f1)), degs = ( deg s) as Nat by A1, Lm8;

 ( deg (t1 - t2)) <= ( max (( deg t1),( deg ( - t2)))) by Th22;

 then

 A61: ( deg (t1 - t2)) <= ( max (( deg t1),( deg t2))) by POLYNOM4: 8;



 A62: ( deg (t1 - t2)) < degs

 proof

 per cases by XXREAL_0: 16;

 suppose ( max (( deg t1),( deg t2))) = ( deg t1);

 hence thesis by A54, A61, XXREAL_0: 2;

 end;

 suppose ( max (( deg t1),( deg t2))) = ( deg t2);

 hence thesis by A56, A61, XXREAL_0: 2;

 end;

 end;

 ( deg (t1 - t2)) = (d + degs) by A1, A58, A57, A60, Th23;

 hence contradiction by A62, NAT_1: 11;

 end;

 hence thesis;

 end;

 end

 definition

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

 let p,s be Polynomial of L;

 :: HURWITZ:def6

 func p mod s -> Polynomial of L equals (p - ((p div s) *' s));

 coherence ;

 end

 definition

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

 let p,s be Polynomial of L;

 :: HURWITZ:def7

 pred s divides p means (p mod s) = ( 0_. L);

 end

 theorem :: HURWITZ:34



 Th34: for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non empty doubleLoopStr holds for p,s be Polynomial of L st s <> ( 0_. L) holds s divides p iff ex t be Polynomial of L st (t *' s) = p

 proof

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

 let p,s be Polynomial of L;

 assume

 A1: s <> ( 0_. L);

 A2:

 now

 (( deg s) - 0 ) > ( 0 - 1) by A1, Lm8;

 then

 A3: ( deg ( 0_. L)) < ( deg s) by Th20;

 given t be Polynomial of L such that

 A4: (t *' s) = p;

 p = ((t *' s) + ( 0_. L)) by A4, POLYNOM3: 28;

 then (p div s) = t by A3, Def5;

 then (p mod s) = ( 0_. L) by A4, POLYNOM3: 29;

 hence s divides p;

 end;

 now

 assume

 A5: s divides p;

 consider t be Polynomial of L such that

 A6: p = (((p div s) *' s) + t) and ( deg t) < ( deg s) by A1, Def5;

 (p mod s) = (t + (((p div s) *' s) - ((p div s) *' s))) by A6, POLYNOM3: 26

 .= (t + ( 0_. L)) by POLYNOM3: 29

 .= t by POLYNOM3: 28;

 then t = ( 0_. L) by A5;

 then p = ((p div s) *' s) by A6, POLYNOM3: 28;

 hence ex t be Polynomial of L st (t *' s) = p;

 end;

 hence thesis by A2;

 end;

 theorem :: HURWITZ:35

 for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non degenerated non empty doubleLoopStr holds for p be Polynomial of L holds for z be Element of L st z is_a_root_of p holds ( rpoly (1,z)) divides p

 proof

 let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non degenerated non empty doubleLoopStr, p be Polynomial of L;

 let z be Element of L;

 (( rpoly (1,z)) . 1) = ( 1_ L) by Lm10;

 then

 A1: ( rpoly (1,z)) <> ( 0_. L);

 assume z is_a_root_of p;

 then ex s be Polynomial of L st p = (( rpoly (1,z)) *' s) by Th33;

 hence thesis by A1, Th34;

 end;

 theorem :: HURWITZ:36

 for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non degenerated non empty doubleLoopStr holds for p be Polynomial of L holds for z be Element of L st p <> ( 0_. L) & z is_a_root_of p holds ( deg (p div ( rpoly (1,z)))) = (( deg p) - 1)

 proof

 let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non degenerated non empty doubleLoopStr, p be Polynomial of L;

 let z be Element of L;

 assume that

 A1: p <> ( 0_. L) and

 A2: z is_a_root_of p;

 consider s be Polynomial of L such that

 A3: p = (( rpoly (1,z)) *' s) by A2, Th33;



 A4: ( rpoly (1,z)) <> ( 0_. L) by A1, A3, POLYNOM4: 2;



 A5: ex t be Polynomial of L st p = ((s *' ( rpoly (1,z))) + t) & ( deg t) < ( deg ( rpoly (1,z)))

 proof

 take t = ( 0_. L);

 thus ((s *' ( rpoly (1,z))) + t) = p by A3, POLYNOM3: 28;

 ( deg t) = ( - 1) by Th20;

 hence thesis by Th27;

 end;

 s <> ( 0_. L) by A1, A3, POLYNOM3: 34;



 then ( deg p) = (( deg ( rpoly (1,z))) + ( deg s)) by A3, A4, Th23

 .= (1 + ( deg s)) by Th27;

 hence thesis by A4, A5, Def5;

 end;

 begin

 definition

 let f be Polynomial of F_Complex ;

 :: HURWITZ:def8

 attr f is Hurwitz means for z be Element of F_Complex st z is_a_root_of f holds ( Re z) < 0 ;

 end

 theorem :: HURWITZ:37

 ( 0_. F_Complex ) is non Hurwitz

 proof

 ( eval (( 0_. F_Complex ),( 1_ F_Complex ))) = ( 0. F_Complex ) by POLYNOM4: 17;

 then ( 1_ F_Complex ) is_a_root_of ( 0_. F_Complex ) by POLYNOM5:def 7;

 hence thesis by COMPLEX1: 6, COMPLFLD: 8;

 end;

 theorem :: HURWITZ:38

 for x be Element of F_Complex st x <> ( 0. F_Complex ) holds (x * ( 1_. F_Complex )) is Hurwitz

 proof

 let x be Element of F_Complex ;

 set p = (x * ( 1_. F_Complex ));

 assume

 A1: x <> ( 0. F_Complex );

 now

 let z be Element of F_Complex ;

 assume z is_a_root_of p;

 then

 A2: ( eval (p,z)) = ( 0. F_Complex ) by POLYNOM5:def 7;

 ( eval (p,z)) = (x * ( eval (( 1_. F_Complex ),z))) by POLYNOM5: 30

 .= (x * ( 1_ F_Complex )) by POLYNOM4: 18;

 hence ( Re z) < 0 by A1, A2;

 end;

 hence thesis;

 end;

 theorem :: HURWITZ:39



 Th39: for x,z be Element of F_Complex st x <> ( 0. F_Complex ) holds (x * ( rpoly (1,z))) is Hurwitz iff ( Re z) < 0

 proof

 let x,z be Element of F_Complex ;

 set p = (x * ( rpoly (1,z)));

 assume

 A1: x <> ( 0. F_Complex );

 A2:

 now

 assume

 A3: ( Re z) < 0 ;

 now

 let y be Element of F_Complex ;

 assume y is_a_root_of p;



 then ( 0. F_Complex ) = ( eval (p,y)) by POLYNOM5:def 7

 .= (x * ( eval (( rpoly (1,z)),y))) by POLYNOM5: 30

 .= (x * (y - z)) by Th29;

 then (y - z) = ( 0. F_Complex ) by A1, VECTSP_1: 12;

 hence ( Re y) < 0 by A3, RLVECT_1: 21;

 end;

 hence p is Hurwitz;

 end;

 now

 ( eval (p,z)) = (x * ( eval (( rpoly (1,z)),z))) by POLYNOM5: 30

 .= (x * (z - z)) by Th29

 .= (x * ( 0. F_Complex )) by RLVECT_1: 15

 .= ( 0. F_Complex );

 then

 A4: z is_a_root_of p by POLYNOM5:def 7;

 assume (x * ( rpoly (1,z))) is Hurwitz;

 hence ( Re z) < 0 by A4;

 end;

 hence thesis by A2;

 end;

 theorem :: HURWITZ:40



 Th40: for f be Polynomial of F_Complex holds for z be Element of F_Complex st z <> ( 0. F_Complex ) holds f is Hurwitz iff (z * f) is Hurwitz

 proof

 let f be Polynomial of F_Complex ;

 let z be Element of F_Complex ;

 assume

 A1: z <> ( 0. F_Complex );

 A2:

 now

 assume

 A3: f is Hurwitz;

 now

 let x be Element of F_Complex ;

 assume x is_a_root_of (z * f);



 then ( 0. F_Complex ) = ( eval ((z * f),x)) by POLYNOM5:def 7

 .= (z * ( eval (f,x))) by POLYNOM5: 30;

 then ( eval (f,x)) = ( 0. F_Complex ) by A1, VECTSP_1: 12;

 then x is_a_root_of f by POLYNOM5:def 7;

 hence ( Re x) < 0 by A3;

 end;

 hence (z * f) is Hurwitz;

 end;

 now

 assume

 A4: (z * f) is Hurwitz;

 now

 let x be Element of F_Complex ;

 assume

 A5: x is_a_root_of f;

 ( eval ((z * f),x)) = (z * ( eval (f,x))) by POLYNOM5: 30

 .= (z * ( 0. F_Complex )) by A5, POLYNOM5:def 7

 .= ( 0. F_Complex );

 then x is_a_root_of (z * f) by POLYNOM5:def 7;

 hence ( Re x) < 0 by A4;

 end;

 hence f is Hurwitz;

 end;

 hence thesis by A2;

 end;



 Lm12: for f,g,h be Polynomial of F_Complex st f = (g *' h) holds for x be Element of F_Complex holds (x is_a_root_of g or x is_a_root_of h) implies x is_a_root_of f

 proof

 let f,g,h be Polynomial of F_Complex ;

 assume

 A1: f = (g *' h);

 let x be Element of F_Complex ;



 A2: ( eval (f,x)) = (( eval (g,x)) * ( eval (h,x))) by A1, POLYNOM4: 24;

 assume

 A3: x is_a_root_of g or x is_a_root_of h;

 per cases by A3;

 suppose x is_a_root_of g;

 then ( eval (g,x)) = ( 0. F_Complex ) by POLYNOM5:def 7;

 then ( eval (f,x)) = ( 0. F_Complex ) by A2;

 hence thesis by POLYNOM5:def 7;

 end;

 suppose x is_a_root_of h;

 then ( eval (h,x)) = ( 0. F_Complex ) by POLYNOM5:def 7;

 then ( eval (f,x)) = ( 0. F_Complex ) by A2;

 hence thesis by POLYNOM5:def 7;

 end;

 end;

 theorem :: HURWITZ:41



 Th41: for f,g be Polynomial of F_Complex holds (f *' g) is Hurwitz iff f is Hurwitz & g is Hurwitz

 proof

 let f,g be Polynomial of F_Complex ;

 A1:

 now

 assume that

 A2: f is Hurwitz and

 A3: g is Hurwitz;

 now

 let z be Element of F_Complex ;

 assume z is_a_root_of (f *' g);



 then

 A4: ( 0. F_Complex ) = ( eval ((f *' g),z)) by POLYNOM5:def 7

 .= (( eval (f,z)) * ( eval (g,z))) by POLYNOM4: 24;

 per cases by A4, VECTSP_1: 12;

 suppose ( eval (f,z)) = ( 0. F_Complex );

 then z is_a_root_of f by POLYNOM5:def 7;

 hence ( Re z) < 0 by A2;

 end;

 suppose ( eval (g,z)) = ( 0. F_Complex );

 then z is_a_root_of g by POLYNOM5:def 7;

 hence ( Re z) < 0 by A3;

 end;

 end;

 hence (f *' g) is Hurwitz;

 end;

 now

 assume

 A5: (f *' g) is Hurwitz;

 now

 let z be Element of F_Complex ;

 assume z is_a_root_of f;

 then z is_a_root_of (f *' g) by Lm12;

 hence ( Re z) < 0 by A5;

 end;

 hence f is Hurwitz;

 now

 let z be Element of F_Complex ;

 assume z is_a_root_of g;

 then z is_a_root_of (f *' g) by Lm12;

 hence ( Re z) < 0 by A5;

 end;

 hence g is Hurwitz;

 end;

 hence thesis by A1;

 end;

 definition

 let f be Polynomial of F_Complex ;

 :: HURWITZ:def9

 func f *' -> Polynomial of F_Complex means

 : Def9: for i be Element of NAT holds (it . i) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * ((f . i) *' ));

 existence

 proof

 defpred P[ object, object] means ex n be Element of NAT st n = $1 & $2 = ((( power F_Complex ) . (( - ( 1_ F_Complex )),n)) * ((f . n) *' ));



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

 proof

 let u be object;

 assume u in NAT ;

 then

 reconsider u9 = u as Element of NAT ;

 take ((( power F_Complex ) . (( - ( 1_ F_Complex )),u9)) * ((f . u9) *' ));

 thus thesis;

 end;

 consider g be sequence of the carrier of F_Complex such that

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

 reconsider g as sequence of F_Complex ;

 ex n be Nat st for i be Nat st i >= n holds (g . i) = ( 0. F_Complex )

 proof

 take n = ( len f);

 now

 let i be Nat;

 reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

 assume

 A3: i >= n;

 ex m be Element of NAT st m = i1 & (g . i1) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),m)) * ((f . m) *' )) by A2;



 hence (g . i) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),i1)) * (( 0. F_Complex ) *' )) by A3, ALGSEQ_1: 8

 .= ( 0. F_Complex ) by COMPLFLD: 47;

 end;

 hence thesis;

 end;

 then

 reconsider p = g as AlgSequence of F_Complex by ALGSEQ_1:def 1;

 take p;

 now

 let i be Element of NAT ;

 ex n be Element of NAT st n = i & (p . i) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),n)) * ((f . n) *' )) by A2;

 hence (p . i) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * ((f . i) *' ));

 end;

 hence thesis;

 end;

 uniqueness

 proof

 let z1,z2 be AlgSequence of F_Complex ;

 assume

 A4: for i be Element of NAT holds (z1 . i) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * ((f . i) *' ));

 assume

 A5: for i be Element of NAT holds (z2 . i) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * ((f . i) *' ));

 A6:

 now

 let x be object;

 assume x in ( dom z1);

 then

 reconsider x9 = x as Element of NAT ;



 thus (z1 . x) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),x9)) * ((f . x9) *' )) by A4

 .= (z2 . x) by A5;

 end;

 ( dom z1) = NAT by FUNCT_2:def 1

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

 hence z1 = z2 by A6, FUNCT_1: 2;

 end;

 involutiveness

 proof

 let g,f be Polynomial of F_Complex such that

 A7: for i be Element of NAT holds (g . i) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * ((f . i) *' ));

 let i be Element of NAT ;



 thus (f . i) = (( 1_ F_Complex ) * (f . i))

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),(2 * i))) * (f . i)) by Th4

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),(i + i))) * (f . i))

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * (( power F_Complex ) . (( - ( 1_ F_Complex )),i))) * (f . i)) by Th3

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * (( power F_Complex ) . ((( - ( 1_ F_Complex )) *' ),i))) * (f . i)) by Lm2, COMPLEX1: 38

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) *' )) * (f . i)) by Th5

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * (((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) *' ) * (((f . i) *' ) *' )))

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * (((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * ((f . i) *' )) *' )) by COMPLFLD: 54

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),i)) * ((g . i) *' )) by A7;

 end;

 end

 theorem :: HURWITZ:42



 Th42: for f be Polynomial of F_Complex holds ( deg (f *' )) = ( deg f)

 proof

 let f be Polynomial of F_Complex ;



 A1: for k be Nat holds (f . k) = ( 0. F_Complex ) iff ((f *' ) . k) = ( 0. F_Complex )

 proof

 let k be Nat;

 reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

 hereby

 assume (f . k) = ( 0. F_Complex );



 hence ((f *' ) . k) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),k1)) * ( 0. F_Complex )) by Def9, COMPLFLD: 47

 .= ( 0. F_Complex );

 end;

 assume ((f *' ) . k) = ( 0. F_Complex );

 then

 A2: ( 0. F_Complex ) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),k1)) * ((f . k) *' )) by Def9;

 (( power F_Complex ) . (( - ( 1_ F_Complex )),k1)) <> ( 0. F_Complex ) by Th2;

 then ((f . k) *' ) = ( 0. F_Complex ) by A2, VECTSP_1: 12;

 hence thesis by COMPLEX1: 28, COMPLFLD: 7;

 end;

 A3:

 now

 assume

 A4: ( len f) > ( len (f *' ));

 then (( len f) + 1) > ( 0 + 1) by XREAL_1: 6;

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

 then

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

 (l + 1) > ( len (f *' )) by A4;

 then l >= ( len (f *' )) by NAT_1: 13;

 then

 A5: ((f *' ) . l) = ( 0. F_Complex ) by ALGSEQ_1: 8;

 ( len f) = (l + 1);

 then (f . l) <> ( 0. F_Complex ) by ALGSEQ_1: 10;

 hence contradiction by A1, A5;

 end;

 now

 let i be Nat;

 assume i >= ( len f);

 then (f . i) = ( 0. F_Complex ) by ALGSEQ_1: 8;

 hence ((f *' ) . i) = ( 0. F_Complex ) by A1;

 end;

 then ( len f) is_at_least_length_of (f *' ) by ALGSEQ_1:def 2;

 then ( len f) >= ( len (f *' )) by ALGSEQ_1:def 3;

 hence thesis by A3, XXREAL_0: 1;

 end;

 ::$Canceled

 theorem :: HURWITZ:44



 Th43: for f be Polynomial of F_Complex holds for z be Element of F_Complex holds ((z * f) *' ) = ((z *' ) * (f *' ))

 proof

 let f be Polynomial of F_Complex ;

 let x be Element of F_Complex ;

 set g1 = (x * f), g2 = ((x *' ) * (f *' ));

 A1:

 now

 let k9 be object;

 assume k9 in ( dom (g1 *' ));

 then

 reconsider k = k9 as Element of NAT ;

 (g1 . k) = (x * (f . k)) by POLYNOM5:def 4;



 then ((g1 *' ) . k) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ((x * (f . k)) *' )) by Def9

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ((x *' ) * ((f . k) *' ))) by COMPLFLD: 54

 .= ((x *' ) * ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ((f . k) *' )))

 .= ((x *' ) * ((f *' ) . k)) by Def9;

 hence ((g1 *' ) . k9) = (g2 . k9) by POLYNOM5:def 4;

 end;

 ( dom (g1 *' )) = NAT by FUNCT_2:def 1

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

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:45



 Th44: for f be Polynomial of F_Complex holds (( - f) *' ) = ( - (f *' ))

 proof

 let f be Polynomial of F_Complex ;

 set h1 = ( - f);

 A1:

 now

 let k9 be object;

 assume k9 in ( dom (h1 *' ));

 then

 reconsider k = k9 as Element of NAT ;

 (h1 . k) = ( - (f . k)) by BHSP_1: 44;



 then ((h1 *' ) . k) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * (( - (f . k)) *' )) by Def9

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ( - ((f . k) *' ))) by COMPLFLD: 52

 .= ( - ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ((f . k) *' ))) by VECTSP_1: 8

 .= ( - ((f *' ) . k)) by Def9;

 hence ((h1 *' ) . k9) = (( - (f *' )) . k9) by BHSP_1: 44;

 end;

 ( dom (h1 *' )) = NAT by FUNCT_2:def 1

 .= ( dom ( - (f *' ))) by FUNCT_2:def 1;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:46



 Th45: for f,g be Polynomial of F_Complex holds ((f + g) *' ) = ((f *' ) + (g *' ))

 proof

 let f,g be Polynomial of F_Complex ;

 set h1 = (f + g);

 A1:

 now

 let k9 be object;

 assume k9 in ( dom (h1 *' ));

 then

 reconsider k = k9 as Element of NAT ;

 (h1 . k) = ((f . k) + (g . k)) by NORMSP_1:def 2;



 then ((h1 *' ) . k) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * (((f . k) + (g . k)) *' )) by Def9

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * (((f . k) *' ) + ((g . k) *' ))) by COMPLFLD: 51

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ((f . k) *' )) + ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ((g . k) *' )))

 .= (((f *' ) . k) + ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ((g . k) *' ))) by Def9

 .= (((f *' ) . k) + ((g *' ) . k)) by Def9;

 hence ((h1 *' ) . k9) = (((f *' ) + (g *' )) . k9) by NORMSP_1:def 2;

 end;

 ( dom (h1 *' )) = NAT by FUNCT_2:def 1

 .= ( dom ((f *' ) + (g *' ))) by FUNCT_2:def 1;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ:47



 Th46: for f,g be Polynomial of F_Complex holds ((f *' g) *' ) = ((f *' ) *' (g *' ))

 proof

 let f,g be Polynomial of F_Complex ;

 set h1 = (f *' g);

 A1:

 now

 let k9 be object;

 assume k9 in ( dom (h1 *' ));

 then

 reconsider k = k9 as Element of NAT ;

 consider s be FinSequence of F_Complex such that

 A2: ( len s) = (k + 1) and

 A3: (h1 . k) = ( Sum s) and

 A4: for j be Element of NAT st j in ( dom s) holds (s . j) = ((f . (j -' 1)) * (g . ((k + 1) -' j))) by POLYNOM3:def 9;

 defpred P[ set, set] means $2 = ((s /. $1) *' );

 consider t be FinSequence of F_Complex such that

 A5: ( len t) = (k + 1) and

 A6: (((f *' ) *' (g *' )) . k) = ( Sum t) and

 A7: for j be Element of NAT st j in ( dom t) holds (t . j) = (((f *' ) . (j -' 1)) * ((g *' ) . ((k + 1) -' j))) by POLYNOM3:def 9;



 A8: for j be Nat st j in ( Seg ( len s)) holds ex x be Element of F_Complex st P[j, x];

 consider u be FinSequence of F_Complex such that

 A9: ( dom u) = ( Seg ( len s)) & for j be Nat st j in ( Seg ( len s)) holds P[j, (u . j)] from FINSEQ_1:sch 5( A8);

 A10:

 now

 let j be Element of NAT ;

 assume

 A11: j in ( dom u);



 hence (u /. j) = (u . j) by PARTFUN1:def 6

 .= ((s /. j) *' ) by A9, A11;

 end;



 A12: ( dom u) = ( Seg ( len t)) by A2, A5, A9

 .= ( dom t) by FINSEQ_1:def 3;



 A13: ( dom s) = ( Seg ( len t)) by A2, A5, FINSEQ_1:def 3

 .= ( dom t) by FINSEQ_1:def 3;

 A14:

 now

 let j be Element of NAT ;

 assume

 A15: j in ( dom t);

 then (s . j) = (s /. j) by A13, PARTFUN1:def 6;

 then

 A16: ((s /. j) *' ) = (((f . (j -' 1)) * (g . ((k + 1) -' j))) *' ) by A4, A13, A15;



 A17: j in ( Seg ( len t)) by A15, FINSEQ_1:def 3;

 then j <= (k + 1) by A5, FINSEQ_1: 1;

 then

 A18: ((k + 1) - j) >= (j - j) by XREAL_1: 9;

 1 <= j by A17, FINSEQ_1: 1;

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



 then

 A19: ((j -' 1) + ((k + 1) -' j)) = ((j - 1) + ((k + 1) -' j)) by XREAL_0:def 2

 .= ((j - 1) + ((k + 1) - j)) by A18, XREAL_0:def 2

 .= k;



 thus (t . j) = (((f *' ) . (j -' 1)) * ((g *' ) . ((k + 1) -' j))) by A7, A15

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),(j -' 1))) * ((f . (j -' 1)) *' )) * ((g *' ) . ((k + 1) -' j))) by Def9

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),(j -' 1))) * ((f . (j -' 1)) *' )) * ((( power F_Complex ) . (( - ( 1_ F_Complex )),((k + 1) -' j))) * ((g . ((k + 1) -' j)) *' ))) by Def9

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),(j -' 1))) * (( power F_Complex ) . (( - ( 1_ F_Complex )),((k + 1) -' j)))) * (((f . (j -' 1)) *' ) * ((g . ((k + 1) -' j)) *' )))

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * (((f . (j -' 1)) *' ) * ((g . ((k + 1) -' j)) *' ))) by A19, Th3

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ((s /. j) *' )) by A16, COMPLFLD: 54;

 end;



 A20: ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * u) = t

 proof

 set b = (( power F_Complex ) . (( - ( 1_ F_Complex )),k));

 set a = (b * u);



 A21: ( dom a) = ( dom u) by POLYNOM1:def 1;

 now

 let j be Nat;

 assume

 A22: j in ( dom t);



 hence (a . j) = (a /. j) by A12, A21, PARTFUN1:def 6

 .= (b * (u /. j)) by A12, A22, POLYNOM1:def 1

 .= (b * ((s /. j) *' )) by A10, A12, A22

 .= (t . j) by A14, A22;

 end;

 hence thesis by A12, A21, FINSEQ_1: 13;

 end;

 ( len u) = ( len s) by A9, FINSEQ_1:def 3;

 then ( Sum u) = (( Sum s) *' ) by A10, Th6;



 then ((h1 *' ) . k) = ((( power F_Complex ) . (( - ( 1_ F_Complex )),k)) * ( Sum u)) by A3, Def9

 .= (((f *' ) *' (g *' )) . k) by A6, A20, Th8;

 hence ((h1 *' ) . k9) = (((f *' ) *' (g *' )) . k9);

 end;

 ( dom (h1 *' )) = NAT by FUNCT_2:def 1

 .= ( dom ((f *' ) *' (g *' ))) by FUNCT_2:def 1;

 hence thesis by A1, FUNCT_1: 2;

 end;



 Lm13: for x,xv be Element of COMPLEX holds for u,v,uv,vv be Element of REAL st x = (u + (v * )) & xv = (uv + (vv * )) holds (( |.(x + (xv *' )).| ^2 ) - ( |.(x - xv).| ^2 )) = ((4 * u) * uv)

 proof

 let x,xv be Element of COMPLEX , u,v,uv,vv be Element of REAL ;

 assume that

 A1: x = (u + (v * )) and

 A2: xv = (uv + (vv * ));



 A3: ((u + uv) ^2 ) >= 0 by XREAL_1: 63;



 A4: ((v + ( - vv)) ^2 ) >= 0 by XREAL_1: 63;

 |.(x + (xv *' )).| = ( sqrt (((( Re x) + ( Re (xv *' ))) ^2 ) + (( Im (x + (xv *' ))) ^2 ))) by COMPLEX1: 8

 .= ( sqrt (((u + ( Re (xv *' ))) ^2 ) + (( Im (x + (xv *' ))) ^2 ))) by A1, COMPLEX1: 12

 .= ( sqrt (((u + ( Re xv)) ^2 ) + (( Im (x + (xv *' ))) ^2 ))) by COMPLEX1: 27

 .= ( sqrt (((u + uv) ^2 ) + (( Im (x + (xv *' ))) ^2 ))) by A2, COMPLEX1: 12

 .= ( sqrt (((u + uv) ^2 ) + ((( Im x) + ( Im (xv *' ))) ^2 ))) by COMPLEX1: 8

 .= ( sqrt (((u + uv) ^2 ) + ((v + ( Im (xv *' ))) ^2 ))) by A1, COMPLEX1: 12

 .= ( sqrt (((u + uv) ^2 ) + ((v + ( - ( Im xv))) ^2 ))) by COMPLEX1: 27

 .= ( sqrt (((u + uv) ^2 ) + ((v + ( - vv)) ^2 ))) by A2, COMPLEX1: 12;

 then

 A5: ( |.(x + (xv *' )).| ^2 ) = (((u + uv) ^2 ) + ((v + ( - vv)) ^2 )) by A3, A4, SQUARE_1:def 2;



 A6: ((u - uv) ^2 ) >= 0 by XREAL_1: 63;



 A7: ((((u + uv) ^2 ) + ((v + ( - vv)) ^2 )) - (((u - uv) ^2 ) + ((v - vv) ^2 ))) = ((4 * u) * uv);



 A8: ((v - vv) ^2 ) >= 0 by XREAL_1: 63;

 |.(x - xv).| = ( sqrt (((( Re x) - ( Re xv)) ^2 ) + (( Im (x - xv)) ^2 ))) by COMPLEX1: 19

 .= ( sqrt (((u - ( Re xv)) ^2 ) + (( Im (x - xv)) ^2 ))) by A1, COMPLEX1: 12

 .= ( sqrt (((u - uv) ^2 ) + (( Im (x - xv)) ^2 ))) by A2, COMPLEX1: 12

 .= ( sqrt (((u - uv) ^2 ) + ((( Im x) - ( Im xv)) ^2 ))) by COMPLEX1: 19

 .= ( sqrt (((u - uv) ^2 ) + ((v - ( Im xv)) ^2 ))) by A1, COMPLEX1: 12

 .= ( sqrt (((u - uv) ^2 ) + ((v - vv) ^2 ))) by A2, COMPLEX1: 12;

 hence thesis by A5, A6, A8, A7, SQUARE_1:def 2;

 end;



 Lm14: for x,xv be Element of COMPLEX holds for u,v,uv,vv be Element of REAL st x = (u + (v * )) & xv = (uv + (vv * )) & uv < 0 holds (u < 0 implies |.(x - xv).| < |.(x + (xv *' )).|) & (u > 0 implies |.(x - xv).| > |.(x + (xv *' )).|) & (u = 0 implies |.(x - xv).| = |.(x + (xv *' )).|)

 proof

 let x,xv be Element of COMPLEX , u,v,uv,vv be Element of REAL ;

 assume that

 A1: x = (u + (v * )) and

 A2: xv = (uv + (vv * )) and

 A3: uv < 0 ;

 now

 assume u < 0 ;

 then ((4 * u) * uv) > 0 by A3;

 then (( |.(x + (xv *' )).| ^2 ) - ( |.(x - xv).| ^2 )) > 0 by A1, A2, Lm13;

 then

 A4: ((( |.(x + (xv *' )).| ^2 ) - ( |.(x - xv).| ^2 )) + ( |.(x - xv).| ^2 )) > ( 0 + ( |.(x - xv).| ^2 )) by XREAL_1: 6;

 0 <= |.(x + (xv *' )).| by COMPLEX1: 46;

 hence |.(x + (xv *' )).| > |.(x - xv).| by A4, XREAL_1: 66;

 end;

 hence u < 0 implies |.(x - xv).| < |.(x + (xv *' )).|;

 now

 assume u > 0 ;

 then ((4 * u) * uv) < 0 by A3;

 then (( |.(x + (xv *' )).| ^2 ) - ( |.(x - xv).| ^2 )) < 0 by A1, A2, Lm13;

 then

 A5: ((( |.(x + (xv *' )).| ^2 ) - ( |.(x - xv).| ^2 )) + ( |.(x - xv).| ^2 )) < ( 0 + ( |.(x - xv).| ^2 )) by XREAL_1: 6;

 0 <= |.(x - xv).| by COMPLEX1: 46;

 hence |.(x + (xv *' )).| < |.(x - xv).| by A5, XREAL_1: 66;

 end;

 hence u > 0 implies |.(x - xv).| > |.(x + (xv *' )).|;

 now

 assume u = 0 ;

 then ((4 * u) * uv) = 0 ;

 then

 A6: (( |.(x + (xv *' )).| ^2 ) - ( |.(x - xv).| ^2 )) = 0 by A1, A2, Lm13;

 now

 assume

 A7: |.(x - xv).| <> |.(x + (xv *' )).|;

 per cases by A7, XXREAL_0: 1;

 suppose |.(x - xv).| > |.(x + (xv *' )).|;

 hence contradiction by A6, COMPLEX1: 46, SQUARE_1: 16;

 end;

 suppose |.(x - xv).| < |.(x + (xv *' )).|;

 hence contradiction by A6, COMPLEX1: 46, SQUARE_1: 16;

 end;

 end;

 hence |.(x - xv).| = |.(x + (xv *' )).|;

 end;

 hence thesis;

 end;

 theorem :: HURWITZ:48



 Th47: for x,z be Element of F_Complex holds ( eval ((( rpoly (1,z)) *' ),x)) = (( - x) - (z *' ))

 proof

 let x,z be Element of F_Complex ;

 set p = (( rpoly (1,z)) *' );

 consider F be FinSequence of F_Complex such that

 A1: ( eval (p,x)) = ( Sum F) and

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

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



 A4: ( deg p) = ( deg ( rpoly (1,z))) by Th42

 .= 1 by Th27;



 then

 A5: F = <*(F . 1), (F . 2)*> by A2, FINSEQ_1: 44

 .= ( <*(F . 1)*> ^ <*(F . 2)*>);

 ( len p) = (1 + 1) by A4;

 then 1 in ( Seg ( len F)) by A2;

 then

 A6: 1 in ( dom F) by FINSEQ_1:def 3;



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

 2 in ( Seg ( len F)) by A2, A4;

 then 2 in ( dom F) by FINSEQ_1:def 3;



 then

 A8: (F . 2) = ((p . 1) * (( power F_Complex ) . (x,(1 + 0 )))) by A3, A7

 .= ((p . 1) * ((( power F_Complex ) . (x, 0 )) * x)) by GROUP_1:def 7

 .= ((p . 1) * (( 1_ F_Complex ) * x)) by GROUP_1:def 7

 .= ((p . 1) * x)

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),1)) * ((( rpoly (1,z)) . 1) *' )) * x) by Def9

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )),1)) * ( 1_ F_Complex )) * x) by Lm10, COMPLFLD: 49

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )),(1 + 0 ))) * x)

 .= (((( power F_Complex ) . (( - ( 1_ F_Complex )), 0 )) * ( - ( 1_ F_Complex ))) * x) by GROUP_1:def 7

 .= ((( 1_ F_Complex ) * ( - ( 1_ F_Complex ))) * x) by GROUP_1:def 7

 .= (( - ( 1_ F_Complex )) * x)

 .= ( - (( 1_ F_Complex ) * x)) by VECTSP_1: 9

 .= ( - x);



 A9: (( rpoly (1,z)) . 0 ) = ( - (( power F_Complex ) . (z,(1 + 0 )))) by Lm10

 .= ( - ((( power F_Complex ) . (z, 0 )) * z)) by GROUP_1:def 7

 .= ( - (( 1_ F_Complex ) * z)) by GROUP_1:def 7

 .= ( - z);

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



 then (F . 1) = ((p . 0 ) * (( power F_Complex ) . (x, 0 ))) by A3, A6

 .= ((p . 0 ) * ( 1_ F_Complex )) by GROUP_1:def 7

 .= (p . 0 )

 .= ((( power F_Complex ) . (( - ( 1_ F_Complex )), 0 )) * (( - z) *' )) by A9, Def9

 .= (( 1_ F_Complex ) * (( - z) *' )) by GROUP_1:def 7

 .= (( - z) *' )

 .= ( - (z *' )) by COMPLFLD: 52;



 hence ( eval (p,x)) = (( Sum <*( - (z *' ))*>) + ( Sum <*( - x)*>)) by A1, A5, A8, RLVECT_1: 41

 .= (( Sum <*( - (z *' ))*>) + ( - x)) by RLVECT_1: 44

 .= (( - (z *' )) + ( - x)) by RLVECT_1: 44

 .= (( - x) - (z *' )) by RLVECT_1:def 11;

 end;

 theorem :: HURWITZ:49



 Th48: for f be Polynomial of F_Complex st f is Hurwitz holds for x be Element of F_Complex st ( Re x) >= 0 holds 0 < |.( eval (f,x)).|

 proof

 let f be Polynomial of F_Complex ;

 assume

 A1: f is Hurwitz;

 let x be Element of F_Complex ;

 assume

 A2: ( Re x) >= 0 ;

 ( eval (f,x)) <> ( 0. F_Complex ) by A1, A2, POLYNOM5:def 7;

 hence thesis by COMPLEX1: 47, COMPLFLD: 7;

 end;

 theorem :: HURWITZ:50



 Th49: for f be Polynomial of F_Complex st ( deg f) >= 1 & f is Hurwitz holds for x be Element of F_Complex holds (( Re x) < 0 implies |.( eval (f,x)).| < |.( eval ((f *' ),x)).|) & (( Re x) > 0 implies |.( eval (f,x)).| > |.( eval ((f *' ),x)).|) & (( Re x) = 0 implies |.( eval (f,x)).| = |.( eval ((f *' ),x)).|)

 proof

 A1:

 now

 let y,z be Element of F_Complex ;

 assume

 A2: ( rpoly (1,z)) is Hurwitz;

 z is_a_root_of ( rpoly (1,z)) by Th30;

 then

 A3: ( Re z) < 0 by A2;



 A4: y = (( Re y) + (( Im y) * )) by COMPLEX1: 13;



 A5: (y - z) = ( eval (( rpoly (1,z)),y)) by Th29;



 A6: z = (( Re z) + (( Im z) * )) by COMPLEX1: 13;

 reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;



 A7: ( - y) = ( - y9) by COMPLFLD: 2;

 ( eval ((( rpoly (1,z)) *' ),y)) = (( - y) - (z *' )) by Th47;

 then

 A8: ( eval ((( rpoly (1,z)) *' ),y)) = (( - y9) - (z9 *' )) by A7, COMPLFLD: 3;



 A9: |.(y9 + (z9 *' )).| = |.( - (y9 + (z9 *' ))).| by COMPLEX1: 52;

 assume ( Re y) > 0 ;

 then |.(y9 - z9).| > |.(y9 + (z9 *' )).| by A3, A4, A6, Lm14;

 hence |.( eval (( rpoly (1,z)),y)).| > |.( eval ((( rpoly (1,z)) *' ),y)).| by A5, A8, A9, COMPLFLD: 3;

 end;

 A10:

 now

 let a,y,z be Element of F_Complex ;

 assume that

 A11: ( rpoly (1,z)) is Hurwitz and

 A12: a <> ( 0. F_Complex );

 assume

 A13: ( Re y) > 0 ;



 A14: ( |.a.| * |.( eval ((( rpoly (1,z)) *' ),y)).|) = ( |.(a *' ).| * |.( eval ((( rpoly (1,z)) *' ),y)).|) by COMPLEX1: 53

 .= |.((a *' ) * ( eval ((( rpoly (1,z)) *' ),y))).| by COMPLEX1: 65

 .= |.( eval (((a *' ) * (( rpoly (1,z)) *' )),y)).| by POLYNOM5: 30

 .= |.( eval (((a * ( rpoly (1,z))) *' ),y)).| by Th43;



 A15: |.( eval ((a * ( rpoly (1,z))),y)).| = |.(a * ( eval (( rpoly (1,z)),y))).| by POLYNOM5: 30

 .= ( |.a.| * |.( eval (( rpoly (1,z)),y)).|) by COMPLEX1: 65;

 |.a.| > 0 by A12, COMPLEX1: 47, COMPLFLD: 7;

 hence |.( eval ((a * ( rpoly (1,z))),y)).| > |.( eval (((a * ( rpoly (1,z))) *' ),y)).| by A1, A11, A13, A15, A14, XREAL_1: 68;

 end;

 A16:

 now

 let y,z be Element of F_Complex ;

 assume

 A17: ( rpoly (1,z)) is Hurwitz;

 z is_a_root_of ( rpoly (1,z)) by Th30;

 then

 A18: ( Re z) < 0 by A17;



 A19: y = (( Re y) + (( Im y) * )) by COMPLEX1: 13;



 A20: (y - z) = ( eval (( rpoly (1,z)),y)) by Th29;



 A21: z = (( Re z) + (( Im z) * )) by COMPLEX1: 13;

 reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;



 A22: ( - y) = ( - y9) by COMPLFLD: 2;

 ( eval ((( rpoly (1,z)) *' ),y)) = (( - y) - (z *' )) by Th47;

 then

 A23: ( eval ((( rpoly (1,z)) *' ),y)) = (( - y9) - (z9 *' )) by A22, COMPLFLD: 3;



 A24: |.(y9 + (z9 *' )).| = |.( - (y9 + (z9 *' ))).| by COMPLEX1: 52;

 assume ( Re y) < 0 ;

 then |.(y9 - z9).| < |.(y9 + (z9 *' )).| by A18, A19, A21, Lm14;

 hence |.( eval (( rpoly (1,z)),y)).| < |.( eval ((( rpoly (1,z)) *' ),y)).| by A20, A23, A24, COMPLFLD: 3;

 end;

 A25:

 now

 let a,y,z be Element of F_Complex ;

 assume that

 A26: ( rpoly (1,z)) is Hurwitz and

 A27: a <> ( 0. F_Complex );

 assume

 A28: ( Re y) < 0 ;



 A29: ( |.a.| * |.( eval ((( rpoly (1,z)) *' ),y)).|) = ( |.(a *' ).| * |.( eval ((( rpoly (1,z)) *' ),y)).|) by COMPLEX1: 53

 .= |.((a *' ) * ( eval ((( rpoly (1,z)) *' ),y))).| by COMPLEX1: 65

 .= |.( eval (((a *' ) * (( rpoly (1,z)) *' )),y)).| by POLYNOM5: 30

 .= |.( eval (((a * ( rpoly (1,z))) *' ),y)).| by Th43;



 A30: |.( eval ((a * ( rpoly (1,z))),y)).| = |.(a * ( eval (( rpoly (1,z)),y))).| by POLYNOM5: 30

 .= ( |.a.| * |.( eval (( rpoly (1,z)),y)).|) by COMPLEX1: 65;

 |.a.| > 0 by A27, COMPLEX1: 47, COMPLFLD: 7;

 hence |.( eval ((a * ( rpoly (1,z))),y)).| < |.( eval (((a * ( rpoly (1,z))) *' ),y)).| by A16, A26, A28, A30, A29, XREAL_1: 68;

 end;

 defpred P[ Nat] means for f be Polynomial of F_Complex st ( deg f) >= 1 & f is Hurwitz & ( deg f) = $1 holds for x be Element of F_Complex holds (( Re x) < 0 implies |.( eval (f,x)).| < |.( eval ((f *' ),x)).|) & (( Re x) > 0 implies |.( eval (f,x)).| > |.( eval ((f *' ),x)).|) & (( Re x) = 0 implies |.( eval (f,x)).| = |.( eval ((f *' ),x)).|);

 let f be Polynomial of F_Complex ;

 assume that

 A31: ( deg f) >= 1 and

 A32: f is Hurwitz;

 A33:

 now

 let y,z be Element of F_Complex ;

 assume

 A34: ( rpoly (1,z)) is Hurwitz;

 z is_a_root_of ( rpoly (1,z)) by Th30;

 then

 A35: ( Re z) < 0 by A34;



 A36: y = (( Re y) + (( Im y) * )) by COMPLEX1: 13;



 A37: (y - z) = ( eval (( rpoly (1,z)),y)) by Th29;



 A38: z = (( Re z) + (( Im z) * )) by COMPLEX1: 13;

 reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;



 A39: ( - y) = ( - y9) by COMPLFLD: 2;

 ( eval ((( rpoly (1,z)) *' ),y)) = (( - y) - (z *' )) by Th47;

 then

 A40: ( eval ((( rpoly (1,z)) *' ),y)) = (( - y9) - (z9 *' )) by A39, COMPLFLD: 3;



 A41: |.(y9 + (z9 *' )).| = |.( - (y9 + (z9 *' ))).| by COMPLEX1: 52;

 assume ( Re y) = 0 ;

 then |.(y9 - z9).| = |.(y9 + (z9 *' )).| by A35, A36, A38, Lm14;

 hence |.( eval (( rpoly (1,z)),y)).| = |.( eval ((( rpoly (1,z)) *' ),y)).| by A37, A40, A41, COMPLFLD: 3;

 end;

 A42:

 now

 let a,y,z be Element of F_Complex ;

 assume that

 A43: ( rpoly (1,z)) is Hurwitz and a <> ( 0. F_Complex );



 A44: |.( eval ((a * ( rpoly (1,z))),y)).| = |.(a * ( eval (( rpoly (1,z)),y))).| by POLYNOM5: 30

 .= ( |.a.| * |.( eval (( rpoly (1,z)),y)).|) by COMPLEX1: 65;



 A45: ( |.a.| * |.( eval ((( rpoly (1,z)) *' ),y)).|) = ( |.(a *' ).| * |.( eval ((( rpoly (1,z)) *' ),y)).|) by COMPLEX1: 53

 .= |.((a *' ) * ( eval ((( rpoly (1,z)) *' ),y))).| by COMPLEX1: 65

 .= |.( eval (((a *' ) * (( rpoly (1,z)) *' )),y)).| by POLYNOM5: 30

 .= |.( eval (((a * ( rpoly (1,z))) *' ),y)).| by Th43;

 assume ( Re y) = 0 ;

 hence |.( eval ((a * ( rpoly (1,z))),y)).| = |.( eval (((a * ( rpoly (1,z))) *' ),y)).| by A33, A43, A44, A45;

 end;

 A46:

 now

 let k be Nat;

 assume

 A47: P[k];

 now

 let f be Polynomial of F_Complex ;

 assume that

 A48: ( deg f) >= 1 and

 A49: f is Hurwitz and

 A50: ( deg f) = (k + 1);

 let x be Element of F_Complex ;

 per cases by A48, A50, XXREAL_0: 1;

 suppose (k + 1) = 1;

 then

 consider z1,z2 be Element of F_Complex such that

 A51: z1 <> ( 0. F_Complex ) and

 A52: f = (z1 * ( rpoly (1,z2))) by A50, Th28;

 ( rpoly (1,z2)) is Hurwitz by A49, A51, A52, Th40;

 hence (( Re x) < 0 implies |.( eval (f,x)).| < |.( eval ((f *' ),x)).|) & (( Re x) > 0 implies |.( eval (f,x)).| > |.( eval ((f *' ),x)).|) & (( Re x) = 0 implies |.( eval (f,x)).| = |.( eval ((f *' ),x)).|) by A25, A10, A42, A51, A52;

 end;

 suppose

 A53: (k + 1) > 1;



 A54: ((k + 1) + 1) > ((k + 1) + 0 ) by XREAL_1: 6;

 then

 A55: f <> ( 0_. F_Complex ) by A50, POLYNOM4: 3;

 ( len f) > 1 by A48, A50, A54, XXREAL_0: 2;

 then f is with_roots by POLYNOM5: 74;

 then

 consider z be Element of F_Complex such that

 A56: z is_a_root_of f by POLYNOM5:def 8;

 consider f1 be Polynomial of F_Complex such that

 A57: f = (( rpoly (1,z)) *' f1) by A56, Th33;



 A58: f1 <> ( 0_. F_Complex ) by A57, A55, POLYNOM3: 34;

 ( rpoly (1,z)) <> ( 0_. F_Complex ) by A57, A55, POLYNOM3: 34;



 then

 A59: ( deg f) = (( deg ( rpoly (1,z))) + ( deg f1)) by A57, A58, Th23

 .= (1 + ( deg f1)) by Th27;



 A60: ( rpoly (1,z)) is Hurwitz by A49, A57, Th41;



 A61: f1 is Hurwitz by A49, A57, Th41;



 A62: k >= 1 by A53, NAT_1: 13;

 A63:

 now

 reconsider r19 = ( eval ((( rpoly (1,z)) *' ),x)), e19 = ( eval ((f1 *' ),x)) as Element of COMPLEX by COMPLFLD:def 1;

 reconsider r9 = ( eval (( rpoly (1,z)),x)), e9 = ( eval (f1,x)) as Element of COMPLEX by COMPLFLD:def 1;



 A64: (( eval ((( rpoly (1,z)) *' ),x)) * ( eval ((f1 *' ),x))) = ( eval (((( rpoly (1,z)) *' ) *' (f1 *' )),x)) by POLYNOM4: 24;

 assume

 A65: ( Re x) > 0 ;

 then

 A66: |.e9.| > |.e19.| by A47, A50, A59, A61, A62;

 0 <= |.r19.| by COMPLEX1: 46;

 then

 A67: ( |.r19.| * |.e9.|) >= ( |.r19.| * |.e19.|) by A66, XREAL_1: 64;

 0 <= |.e19.| by COMPLEX1: 46;

 then ( |.r9.| * |.e9.|) > ( |.r19.| * |.e9.|) by A1, A60, A65, A66, XREAL_1: 68;

 then ( |.r9.| * |.e9.|) > ( |.r19.| * |.e19.|) by A67, XXREAL_0: 2;

 then |.(r9 * e9).| > ( |.r19.| * |.e19.|) by COMPLEX1: 65;

 then

 A68: |.(( eval (( rpoly (1,z)),x)) * ( eval (f1,x))).| > |.(( eval ((( rpoly (1,z)) *' ),x)) * ( eval ((f1 *' ),x))).| by COMPLEX1: 65;

 (( eval (( rpoly (1,z)),x)) * ( eval (f1,x))) = ( eval ((( rpoly (1,z)) *' f1),x)) by POLYNOM4: 24;

 hence |.( eval (f,x)).| > |.( eval ((f *' ),x)).| by A57, A68, A64, Th46;

 end;

 A69:

 now

 reconsider r19 = ( eval ((( rpoly (1,z)) *' ),x)), e19 = ( eval ((f1 *' ),x)) as Element of COMPLEX by COMPLFLD:def 1;

 reconsider r9 = ( eval (( rpoly (1,z)),x)), e9 = ( eval (f1,x)) as Element of COMPLEX by COMPLFLD:def 1;



 A70: 0 <= |.r9.| by COMPLEX1: 46;

 assume

 A71: ( Re x) < 0 ;

 then

 A72: |.r9.| < |.r19.| by A16, A60;

 0 <= |.e9.| by COMPLEX1: 46;

 then

 A73: ( |.r9.| * |.e9.|) <= ( |.r19.| * |.e9.|) by A72, XREAL_1: 64;

 |.e9.| < |.e19.| by A47, A50, A59, A61, A62, A71;

 then ( |.r19.| * |.e9.|) < ( |.r19.| * |.e19.|) by A72, A70, XREAL_1: 68;

 then ( |.r9.| * |.e9.|) < ( |.r19.| * |.e19.|) by A73, XXREAL_0: 2;

 then |.(r9 * e9).| < ( |.r19.| * |.e19.|) by COMPLEX1: 65;

 then

 A74: |.(( eval (( rpoly (1,z)),x)) * ( eval (f1,x))).| < |.(( eval ((( rpoly (1,z)) *' ),x)) * ( eval ((f1 *' ),x))).| by COMPLEX1: 65;



 A75: (( eval ((( rpoly (1,z)) *' ),x)) * ( eval ((f1 *' ),x))) = ( eval (((( rpoly (1,z)) *' ) *' (f1 *' )),x)) by POLYNOM4: 24;

 (( eval (( rpoly (1,z)),x)) * ( eval (f1,x))) = ( eval ((( rpoly (1,z)) *' f1),x)) by POLYNOM4: 24;

 hence |.( eval (f,x)).| < |.( eval ((f *' ),x)).| by A57, A74, A75, Th46;

 end;

 now

 reconsider r19 = ( eval ((( rpoly (1,z)) *' ),x)), e19 = ( eval ((f1 *' ),x)) as Element of COMPLEX by COMPLFLD:def 1;

 reconsider r9 = ( eval (( rpoly (1,z)),x)), e9 = ( eval (f1,x)) as Element of COMPLEX by COMPLFLD:def 1;



 A76: (( eval ((( rpoly (1,z)) *' ),x)) * ( eval ((f1 *' ),x))) = ( eval (((( rpoly (1,z)) *' ) *' (f1 *' )),x)) by POLYNOM4: 24;

 assume

 A77: ( Re x) = 0 ;

 then |.( eval (f1,x)).| = |.( eval ((f1 *' ),x)).| by A47, A50, A59, A61, A62;

 then ( |.r9.| * |.e9.|) = ( |.r19.| * |.e19.|) by A33, A60, A77;

 then |.(r9 * e9).| = ( |.r19.| * |.e19.|) by COMPLEX1: 65;

 then

 A78: |.(( eval (( rpoly (1,z)),x)) * ( eval (f1,x))).| = |.(( eval ((( rpoly (1,z)) *' ),x)) * ( eval ((f1 *' ),x))).| by COMPLEX1: 65;

 (( eval (( rpoly (1,z)),x)) * ( eval (f1,x))) = ( eval ((( rpoly (1,z)) *' f1),x)) by POLYNOM4: 24;

 hence |.( eval (f,x)).| = |.( eval ((f *' ),x)).| by A57, A78, A76, Th46;

 end;

 hence (( Re x) < 0 implies |.( eval (f,x)).| < |.( eval ((f *' ),x)).|) & (( Re x) > 0 implies |.( eval (f,x)).| > |.( eval ((f *' ),x)).|) & (( Re x) = 0 implies |.( eval (f,x)).| = |.( eval ((f *' ),x)).|) by A69, A63;

 end;

 end;

 hence P[(k + 1)];

 end;

 let x be Element of F_Complex ;



 A79: P[ 0 ];



 A80: for k be Nat holds P[k] from NAT_1:sch 2( A79, A46);

 f <> ( 0_. F_Complex ) by A31, Th20;

 then ( deg f) is Element of NAT by Lm8;

 hence thesis by A31, A32, A80;

 end;

 definition

 let f be Polynomial of F_Complex ;

 let z be Element of F_Complex ;

 :: HURWITZ:def10

 func F* (f,z) -> Polynomial of F_Complex equals ((( eval ((f *' ),z)) * f) - (( eval (f,z)) * (f *' )));

 coherence ;

 end

 theorem :: HURWITZ:51



 Th50: for a,b be Element of F_Complex st |.a.| > |.b.| holds for f be Polynomial of F_Complex st ( deg f) >= 1 holds f is Hurwitz iff ((a * f) - (b * (f *' ))) is Hurwitz

 proof

 let a,b be Element of F_Complex ;

 assume

 A1: |.a.| > |.b.|;

 then

 A2: 0 < |.a.| by COMPLEX1: 46;

 then

 A3: a <> ( 0. F_Complex ) by COMPLEX1: 47, COMPLFLD: 7;

 let f be Polynomial of F_Complex ;

 assume

 A4: ( deg f) >= 1;

 set g = ((a * f) - (b * (f *' )));

 per cases ;

 suppose b = ( 0. F_Complex );



 then g = ((a * f) - ( 0_. F_Complex )) by POLYNOM5: 26

 .= ((a * f) + ( 0_. F_Complex )) by Th9

 .= (a * f) by POLYNOM3: 28;

 hence thesis by A3, Th40;

 end;

 suppose

 A5: b <> ( 0. F_Complex );

 reconsider a9 = a, b9 = b as Element of COMPLEX by COMPLFLD:def 1;

 ((( |.a.| ^2 ) - ( |.b.| ^2 )) " ) in COMPLEX by XCMPLX_0:def 2;

 then

 reconsider zz = ((( |.a.| ^2 ) - ( |.b.| ^2 )) " ) as Element of F_Complex by COMPLFLD:def 1;

 set a1 = ((a *' ) * zz), b1 = ( - (b * zz));

 reconsider a19 = a1, b19 = b1 as Element of COMPLEX by COMPLFLD:def 1;



 A6: ((a *' ) * (b " )) = ((a9 *' ) * (b9 " )) by A5, COMPLFLD: 5;



 A7: b19 = ( - (b9 * ((( |.a.| ^2 ) - ( |.b.| ^2 )) " ))) by COMPLFLD: 2;



 A8: 0 < |.b.| by A5, COMPLEX1: 47, COMPLFLD: 7;

 then ( |.a9.| * |.b9.|) > ( |.b9.| * |.b9.|) by A1, XREAL_1: 68;

 then

 A9: (( |.a9.| ^2 ) - ( |.b9.| ^2 )) <> 0 by A1, A2, XREAL_1: 68;

 then

 A10: ( - b1) <> ( 0. F_Complex ) by A5, COMPLFLD: 7, RLVECT_1: 17;

 A11:

 now

 assume

 A12: f is Hurwitz;

 now

 let z be Element of F_Complex ;

 assume z is_a_root_of g;



 then

 A13: ( 0. F_Complex ) = ( eval (((a * f) - (b * (f *' ))),z)) by POLYNOM5:def 7

 .= (( eval ((a * f),z)) - ( eval ((b * (f *' )),z))) by POLYNOM4: 21

 .= ((a * ( eval (f,z))) - ( eval ((b * (f *' )),z))) by POLYNOM5: 30

 .= ((a * ( eval (f,z))) - (b * ( eval ((f *' ),z)))) by POLYNOM5: 30;

 now



 A14: 0 <= |.b.| by COMPLEX1: 46;



 A15: ( |.a.| * |.( eval (f,z)).|) = |.(a * ( eval (f,z))).| by COMPLEX1: 65;



 A16: ( |.b.| * |.( eval ((f *' ),z)).|) = |.(b * ( eval ((f *' ),z))).| by COMPLEX1: 65;

 assume

 A17: ( Re z) >= 0 ;

 per cases by A17;

 suppose

 A18: ( Re z) = 0 ;

 then

 A19: |.( eval (f,z)).| > 0 by A12, Th48;

 |.( eval (f,z)).| = |.( eval ((f *' ),z)).| by A4, A12, A18, Th49;

 then ( |.a.| * |.( eval (f,z)).|) > ( |.b.| * |.( eval ((f *' ),z)).|) by A1, A19, XREAL_1: 68;

 hence contradiction by A13, A15, A16, VECTSP_1: 19;

 end;

 suppose ( Re z) > 0 ;

 then

 A20: |.( eval (f,z)).| > |.( eval ((f *' ),z)).| by A4, A12, Th49;

 then |.( eval (f,z)).| > 0 by COMPLEX1: 46;

 then

 A21: ( |.a.| * |.( eval (f,z)).|) > ( |.b.| * |.( eval (f,z)).|) by A1, XREAL_1: 68;

 ( |.b.| * |.( eval (f,z)).|) >= ( |.b.| * |.( eval ((f *' ),z)).|) by A14, A20, XREAL_1: 64;

 hence contradiction by A13, A15, A16, A21, VECTSP_1: 19;

 end;

 end;

 hence ( Re z) < 0 ;

 end;

 hence g is Hurwitz;

 end;



 A22: |.a1.| = ( |.(a *' ).| * |.((( |.a.| ^2 ) - ( |.b.| ^2 )) " ).|) by COMPLEX1: 65

 .= ( |.a.| * |.((( |.a.| ^2 ) - ( |.b.| ^2 )) " ).|) by COMPLEX1: 53;

 A23:

 now

 let z be Element of COMPLEX ;



 A24: ( Im (z * (z *' ))) = 0 by COMPLEX1: 40;



 A25: (( Re (z * (z *' ))) + (( Im (z * (z *' ))) * )) = (z * (z *' )) by COMPLEX1: 13;



 A26: (( Im z) ^2 ) >= 0 by XREAL_1: 63;



 A27: (( Re z) ^2 ) >= 0 by XREAL_1: 63;

 ( Re (z * (z *' ))) = ((( Re z) ^2 ) + (( Im z) ^2 )) by COMPLEX1: 40;

 hence ((z *' ) * z) = ( |.z.| ^2 ) by A24, A25, A27, A26, SQUARE_1:def 2;

 end;

 then

 A28: ((b9 *' ) * b9) = ( |.b9.| ^2 );



 A29: ((((a9 *' ) * a9) * (b9 " )) - (b9 *' )) = (((( |.a9.| ^2 ) * (b9 " )) - (b9 *' )) * 1) by A23

 .= (((( |.a9.| ^2 ) * (b9 " )) - (b9 *' )) * (b9 * (b9 " ))) by A5, COMPLFLD: 7, XCMPLX_0:def 7

 .= (((( |.a9.| ^2 ) * ((b9 " ) * b9)) - ( |.b9.| ^2 )) * (b9 " )) by A28

 .= (((( |.a9.| ^2 ) * 1) - ( |.b9.| ^2 )) * (b9 " )) by A5, COMPLFLD: 7, XCMPLX_0:def 7;



 then

 A30: ( - (((((a9 *' ) * a9) * (b9 " )) - (b9 *' )) " )) = ( - (((( |.a9.| ^2 ) - ( |.b9.| ^2 )) " ) * ((b9 " ) " ))) by XCMPLX_1: 204

 .= b19 by COMPLFLD: 2;



 A31: b19 = ( - (b9 * ((( |.a.| ^2 ) - ( |.b.| ^2 )) " ))) by COMPLFLD: 2

 .= (( - b9) * ((( |.a.| ^2 ) - ( |.b.| ^2 )) " ));

 then (b1 " ) = (b19 " ) by A5, A9, COMPLFLD: 5, COMPLFLD: 7;

 then

 A32: ( - (b1 " )) = ( - (b19 " )) by COMPLFLD: 2;

 A33:

 now

 assume

 A34: (b1 " ) = ( 0. F_Complex );

 ((b1 " ) * b1) = ( 1_ F_Complex ) by A5, A9, A31, COMPLFLD: 7, VECTSP_1:def 10;

 hence contradiction by A34;

 end;

 A35:

 now

 assume ( - (b1 " )) = ( 0. F_Complex );

 then ( - ( - (b1 " ))) = ( 0. F_Complex ) by RLVECT_1: 12;

 hence contradiction by A33, RLVECT_1: 17;

 end;

 (b1 " ) = (b19 " ) by A5, A9, A31, COMPLFLD: 5, COMPLFLD: 7;

 then ( - (b1 " )) = ( - (b19 " )) by COMPLFLD: 2;

 then

 A36: (( - (b1 " )) " ) = (( - (b19 " )) " ) by A35, COMPLFLD: 5;

 (( - (b1 " )) " ) = ( - ((b1 " ) " )) by A33, Th1

 .= ( - b1) by A5, A9, A31, COMPLFLD: 7, VECTSP_1: 24;



 then ((( - (b19 " )) " ) * ((a9 *' ) * (b9 " ))) = (( - ( - (b9 * ((( |.a.| ^2 ) - ( |.b.| ^2 )) " )))) * ((a9 *' ) * (b9 " ))) by A7, A36, COMPLFLD: 2

 .= (((b9 * (b9 " )) * ((( |.a.| ^2 ) - ( |.b.| ^2 )) " )) * (a9 *' ))

 .= ((1 * ((( |.a.| ^2 ) - ( |.b.| ^2 )) " )) * (a9 *' )) by A5, COMPLFLD: 7, XCMPLX_0:def 7

 .= a19;

 then

 A37: ((( - (b1 " )) " ) * ((a *' ) * (b " ))) = a1 by A35, A6, A32, COMPLFLD: 5;



 A38: ((a9 *' ) * ((b9 " ) * a9)) = ((a *' ) * ((b " ) * a)) by A5, COMPLFLD: 5;



 A39: |.b1.| = |.( - (b * ((( |.a.| ^2 ) - ( |.b.| ^2 )) " ))).| by COMPLFLD: 2

 .= |.(b * ((( |.a.| ^2 ) - ( |.b.| ^2 )) " )).| by COMPLEX1: 52

 .= ( |.b.| * |.((( |.a.| ^2 ) - ( |.b.| ^2 )) " ).|) by COMPLEX1: 65;

 ( - b1) = ( - b19) by COMPLFLD: 2;



 then

 A40: (( - b19) " ) = (( - b1) " ) by A10, COMPLFLD: 5

 .= ( - (b1 " )) by A5, A9, A31, Th1, COMPLFLD: 7;



 A41: ( |.b.| * |.a.|) > ( |.b.| * |.b.|) by A1, A8, XREAL_1: 68;

 ( |.a.| * |.a.|) > ( |.b.| * |.a.|) by A1, A2, XREAL_1: 68;

 then ( |.a.| ^2 ) > ( |.b.| * |.b.|) by A41, XXREAL_0: 2;

 then

 A42: (( |.a.| ^2 ) - ( |.b.| ^2 )) > (( |.b.| ^2 ) - ( |.b.| ^2 )) by XREAL_1: 9;

 A43:

 now

 assume b19 = ( 0. F_Complex );

 then (( - b) * zz) = ( 0. F_Complex ) by VECTSP_1: 9;

 then ( - b) = ( 0. F_Complex ) by A42, COMPLFLD: 7;

 then b = ( - ( 0. F_Complex )) by RLVECT_1: 17;

 hence contradiction by A5, RLVECT_1: 12;

 end;

 ((b * (f *' )) + g) = ((a * f) + (( - (b * (f *' ))) + (b * (f *' )))) by POLYNOM3: 26

 .= ((a * f) + ((b * (f *' )) - (b * (f *' ))))

 .= ((a * f) + ( 0_. F_Complex )) by POLYNOM3: 29;



 then

 A44: ((a * f) - g) = (((b * (f *' )) + g) - g) by POLYNOM3: 28

 .= ((b * (f *' )) + (g - g)) by POLYNOM3: 26

 .= ((b * (f *' )) + ( 0_. F_Complex )) by POLYNOM3: 29;



 A45: (f *' ) = (( 1_ F_Complex ) * (f *' )) by POLYNOM5: 27

 .= (((b " ) * b) * (f *' )) by A5, VECTSP_1:def 10

 .= ((b " ) * (b * (f *' ))) by Th14

 .= ((b " ) * ((a * f) - g)) by A44, POLYNOM3: 28;

 (g *' ) = (((a * f) *' ) + (( - (b * (f *' ))) *' )) by Th45

 .= (((a * f) *' ) + ( - ((b * (f *' )) *' ))) by Th44

 .= (((a *' ) * (f *' )) + ( - ((b * (f *' )) *' ))) by Th43

 .= (((a *' ) * (f *' )) + ( - ((b *' ) * ((f *' ) *' )))) by Th43

 .= (((a *' ) * (f *' )) + ( - ((b *' ) * f)));



 then (g *' ) = (((a *' ) * (((b " ) * (a * f)) + ((b " ) * ( - g)))) + ( - ((b *' ) * f))) by A45, Th18

 .= ((((a *' ) * ((b " ) * (a * f))) + ((a *' ) * ((b " ) * ( - g)))) + ( - ((b *' ) * f))) by Th18

 .= (((a *' ) * ((b " ) * ( - g))) + (((a *' ) * ((b " ) * (a * f))) + ( - ((b *' ) * f)))) by POLYNOM3: 26

 .= (((a *' ) * ((b " ) * ( - g))) + (((a *' ) * (((b " ) * a) * f)) + ( - ((b *' ) * f)))) by Th14

 .= (((a *' ) * ((b " ) * ( - g))) + ((((a *' ) * ((b " ) * a)) * f) + ( - ((b *' ) * f)))) by Th14

 .= (((a *' ) * ((b " ) * ( - g))) + ((((a *' ) * ((b " ) * a)) * f) + (( - (b *' )) * f))) by Th15

 .= (((a *' ) * ((b " ) * ( - g))) + ((((a *' ) * ((b " ) * a)) + ( - (b *' ))) * f)) by Th17

 .= ((((a *' ) * (b " )) * ( - g)) + ((((a *' ) * ((b " ) * a)) + ( - (b *' ))) * f)) by Th14;



 then

 A46: ((g *' ) + ( - (((a *' ) * (b " )) * ( - g)))) = (((((a *' ) * ((b " ) * a)) + ( - (b *' ))) * f) + ((((a *' ) * (b " )) * ( - g)) - (((a *' ) * (b " )) * ( - g)))) by POLYNOM3: 26

 .= (((((a *' ) * ((b " ) * a)) + ( - (b *' ))) * f) + ( 0_. F_Complex )) by POLYNOM3: 29;



 A47: ( - (b9 *' )) = ( - (b *' )) by COMPLFLD: 2;



 A48: f = (( 1_ F_Complex ) * f) by POLYNOM5: 27

 .= (((( - (b1 " )) " ) * ( - (b1 " ))) * f) by A5, A29, A9, A30, A40, COMPLFLD: 7, VECTSP_1:def 10

 .= ((( - (b1 " )) " ) * (( - (b1 " )) * f)) by Th14

 .= ((( - (b1 " )) " ) * ((g *' ) + ( - (((a *' ) * (b " )) * ( - g))))) by A46, A30, A38, A47, A40, POLYNOM3: 28

 .= (((( - (b1 " )) " ) * (g *' )) + ((( - (b1 " )) " ) * ( - (((a *' ) * (b " )) * ( - g))))) by Th18

 .= (((( - (b1 " )) " ) * (g *' )) + ((( - (b1 " )) " ) * (((a *' ) * (b " )) * ( - ( - g))))) by Th16

 .= (((( - (b1 " )) " ) * (g *' )) + ((( - (b1 " )) " ) * (((a *' ) * (b " )) * g))) by Lm3

 .= (((( - (b1 " )) " ) * (g *' )) + (a1 * g)) by A37, Th14

 .= ((((( - b1) " ) " ) * (g *' )) + (a1 * g)) by A5, A9, A31, Th1, COMPLFLD: 7

 .= ((( - b1) * (g *' )) + (a1 * g)) by A10, VECTSP_1: 24

 .= (( - (b1 * (g *' ))) + (a1 * g)) by Th15;

 then ( deg f) <= ( max (( deg (a1 * g)),( deg ( - (b1 * (g *' )))))) by Th22;

 then

 A49: ( deg f) <= ( max (( deg (a1 * g)),( deg (b1 * (g *' ))))) by POLYNOM4: 8;

 |.((( |.a.| ^2 ) - ( |.b.| ^2 )) " ).| > 0 by A42, COMPLEX1: 47;

 then

 A50: |.a1.| > |.b1.| by A1, A22, A39, XREAL_1: 68;

 then |.a1.| > 0 by COMPLEX1: 46;

 then a1 <> ( 0. F_Complex ) by COMPLEX1: 47, COMPLFLD: 7;

 then ( deg f) <= ( max (( deg g),( deg (b1 * (g *' ))))) by A49, POLYNOM5: 25;

 then ( deg f) <= ( max (( deg g),( deg (g *' )))) by A43, POLYNOM5: 25;

 then ( deg f) <= ( max (( deg g),( deg g))) by Th42;

 then

 A51: ( deg g) >= 1 by A4, XXREAL_0: 2;

 now

 assume

 A52: g is Hurwitz;

 now

 let z be Element of F_Complex ;

 assume z is_a_root_of f;



 then

 A53: ( 0. F_Complex ) = ( eval (((a1 * g) - (b1 * (g *' ))),z)) by A48, POLYNOM5:def 7

 .= (( eval ((a1 * g),z)) - ( eval ((b1 * (g *' )),z))) by POLYNOM4: 21

 .= ((a1 * ( eval (g,z))) - ( eval ((b1 * (g *' )),z))) by POLYNOM5: 30

 .= ((a1 * ( eval (g,z))) - (b1 * ( eval ((g *' ),z)))) by POLYNOM5: 30;

 now



 A54: 0 <= |.b1.| by COMPLEX1: 46;



 A55: ( |.a1.| * |.( eval (g,z)).|) = |.(a1 * ( eval (g,z))).| by COMPLEX1: 65;



 A56: ( |.b1.| * |.( eval ((g *' ),z)).|) = |.(b1 * ( eval ((g *' ),z))).| by COMPLEX1: 65;

 assume

 A57: ( Re z) >= 0 ;

 per cases by A57;

 suppose

 A58: ( Re z) = 0 ;

 then

 A59: |.( eval (g,z)).| > 0 by A52, Th48;

 |.( eval (g,z)).| = |.( eval ((g *' ),z)).| by A51, A52, A58, Th49;

 then ( |.a1.| * |.( eval (g,z)).|) > ( |.b1.| * |.( eval ((g *' ),z)).|) by A50, A59, XREAL_1: 68;

 hence contradiction by A53, A55, A56, VECTSP_1: 19;

 end;

 suppose ( Re z) > 0 ;

 then

 A60: |.( eval (g,z)).| > |.( eval ((g *' ),z)).| by A51, A52, Th49;

 then |.( eval (g,z)).| > 0 by COMPLEX1: 46;

 then

 A61: ( |.a1.| * |.( eval (g,z)).|) > ( |.b1.| * |.( eval (g,z)).|) by A50, XREAL_1: 68;

 ( |.b1.| * |.( eval (g,z)).|) >= ( |.b1.| * |.( eval ((g *' ),z)).|) by A54, A60, XREAL_1: 64;

 hence contradiction by A53, A55, A56, A61, VECTSP_1: 19;

 end;

 end;

 hence ( Re z) < 0 ;

 end;

 hence f is Hurwitz;

 end;

 hence thesis by A11;

 end;

 end;

 theorem :: HURWITZ:52



 Th51: for f be Polynomial of F_Complex st ( deg f) >= 1 holds for rho be Element of F_Complex st ( Re rho) < 0 holds f is Hurwitz implies (( F* (f,rho)) div ( rpoly (1,rho))) is Hurwitz

 proof

 let f be Polynomial of F_Complex ;

 assume

 A1: ( deg f) >= 1;

 let rho be Element of F_Complex ;

 assume

 A2: ( Re rho) < 0 ;

 reconsider ef = ( eval (f,rho)), ef1 = ( eval ((f *' ),rho)) as Element of F_Complex ;

 ( eval (((ef1 * f) - (ef * (f *' ))),rho)) = (( eval ((ef1 * f),rho)) - ( eval ((ef * (f *' )),rho))) by POLYNOM4: 21

 .= ((ef1 * ( eval (f,rho))) - ( eval ((ef * (f *' )),rho))) by POLYNOM5: 30

 .= ((ef1 * ( eval (f,rho))) - (ef * ( eval ((f *' ),rho)))) by POLYNOM5: 30

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

 then rho is_a_root_of ((ef1 * f) - (ef * (f *' ))) by POLYNOM5:def 7;

 then

 consider s be Polynomial of F_Complex such that

 A3: ((ef1 * f) - (ef * (f *' ))) = (( rpoly (1,rho)) *' s) by Th33;

 assume

 A4: f is Hurwitz;

 then |.( eval (f,rho)).| < |.( eval ((f *' ),rho)).| by A1, A2, Th49;

 then ((ef1 * f) - (ef * (f *' ))) is Hurwitz by A1, A4, Th50;

 then

 A5: s is Hurwitz by A3, Th41;

 ( - 1) < ( deg ( rpoly (1,rho))) by Th27;

 then

 A6: ( deg ( 0_. F_Complex )) < ( deg ( rpoly (1,rho))) by Th20;

 ((ef1 * f) - (ef * (f *' ))) = ((s *' ( rpoly (1,rho))) + ( 0_. F_Complex )) by A3, POLYNOM3: 28;

 hence thesis by A5, A6, Def5;

 end;

 theorem :: HURWITZ:53

 for f be Polynomial of F_Complex st ( deg f) >= 1 holds (ex rho be Element of F_Complex st ( Re rho) < 0 & |.( eval (f,rho)).| >= |.( eval ((f *' ),rho)).|) implies f is non Hurwitz by Th49;

 ::$Notion-Name

 theorem :: HURWITZ:54

 for f be Polynomial of F_Complex st ( deg f) >= 1 holds for rho be Element of F_Complex st ( Re rho) < 0 & |.( eval (f,rho)).| < |.( eval ((f *' ),rho)).| holds f is Hurwitz iff (( F* (f,rho)) div ( rpoly (1,rho))) is Hurwitz

 proof

 let f be Polynomial of F_Complex ;

 assume

 A1: ( deg f) >= 1;

 let rho be Element of F_Complex ;

 assume that

 A2: ( Re rho) < 0 and

 A3: |.( eval (f,rho)).| < |.( eval ((f *' ),rho)).|;

 reconsider ef = ( eval (f,rho)), ef1 = ( eval ((f *' ),rho)) as Element of F_Complex ;

 now

 ( - 1) < ( deg ( rpoly (1,rho))) by Th27;

 then

 A4: ( deg ( 0_. F_Complex )) < ( deg ( rpoly (1,rho))) by Th20;

 ( eval (((ef1 * f) - (ef * (f *' ))),rho)) = (( eval ((ef1 * f),rho)) - ( eval ((ef * (f *' )),rho))) by POLYNOM4: 21

 .= ((ef1 * ( eval (f,rho))) - ( eval ((ef * (f *' )),rho))) by POLYNOM5: 30

 .= ((ef1 * ( eval (f,rho))) - (ef * ( eval ((f *' ),rho)))) by POLYNOM5: 30

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

 then rho is_a_root_of ((ef1 * f) - (ef * (f *' ))) by POLYNOM5:def 7;

 then

 consider t be Polynomial of F_Complex such that

 A5: ( F* (f,rho)) = (( rpoly (1,rho)) *' t) by Th33;

 ( F* (f,rho)) = ((( rpoly (1,rho)) *' t) + ( 0_. F_Complex )) by A5, POLYNOM3: 28;

 then

 A6: ( F* (f,rho)) = ((( F* (f,rho)) div ( rpoly (1,rho))) *' ( rpoly (1,rho))) by A5, A4, Def5;

 (( 1_ F_Complex ) * ( rpoly (1,rho))) is Hurwitz by A2, Th39;

 then

 A7: ( rpoly (1,rho)) is Hurwitz by POLYNOM5: 27;

 assume (( F* (f,rho)) div ( rpoly (1,rho))) is Hurwitz;

 then ( F* (f,rho)) is Hurwitz by A6, A7, Th41;

 hence f is Hurwitz by A1, A3, Th50;

 end;

 hence thesis by A1, A2, Th51;

 end;