:: RATFUNC1 semantic presentation begin theorem df: :: RATFUNC1:1 for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr for a being Element of L for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds q /. i = a * (p /. i) ) holds Sum q = a * (Sum p) proof let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of L for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds q /. i = a * (p /. i) ) holds Sum q = a * (Sum p) let a be Element of L; ::_thesis: for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds q /. i = a * (p /. i) ) holds Sum q = a * (Sum p) let p, q be FinSequence of L; ::_thesis: ( len p = len q & ( for i being Element of NAT st i in dom p holds q /. i = a * (p /. i) ) implies Sum q = a * (Sum p) ) assume AS: ( len p = len q & ( for i being Element of NAT st i in dom p holds q /. i = a * (p /. i) ) ) ; ::_thesis: Sum q = a * (Sum p) consider fq being Function of NAT, the carrier of L such that A6: Sum q = fq . (len q) and A7: fq . 0 = 0. L and A8: for j being Element of NAT for v being Element of L st j < len q & v = q . (j + 1) holds fq . (j + 1) = (fq . j) + v by RLVECT_1:def_12; consider fp being Function of NAT, the carrier of L such that A12: Sum p = fp . (len p) and A13: fp . 0 = 0. L and A14: for j being Element of NAT for v being Element of L st j < len p & v = p . (j + 1) holds fp . (j + 1) = (fp . j) + v by RLVECT_1:def_12; defpred S1[ Element of NAT ] means fq . $1 = a * (fp . $1); B1: S1[ 0 ] by A13, A7, VECTSP_1:6; B2: for j being Element of NAT st 0 <= j & j < len p & S1[j] holds S1[j + 1] proof let j be Element of NAT ; ::_thesis: ( 0 <= j & j < len p & S1[j] implies S1[j + 1] ) assume A18: ( 0 <= j & j < len p ) ; ::_thesis: ( not S1[j] or S1[j + 1] ) assume A19: S1[j] ; ::_thesis: S1[j + 1] B3: 1 <= j + 1 by NAT_1:11; B4: j + 1 <= len p by A18, NAT_1:13; then j + 1 in Seg (len q) by B3, AS; then A20: j + 1 in dom q by FINSEQ_1:def_3; j + 1 in Seg (len p) by B3, B4; then A20a: j + 1 in dom p by FINSEQ_1:def_3; set vq = q /. (j + 1); set vp = p /. (j + 1); A21: q /. (j + 1) = q . (j + 1) by A20, PARTFUN1:def_6; A21a: p /. (j + 1) = p . (j + 1) by A20a, PARTFUN1:def_6; fq . (j + 1) = (a * (fp . j)) + (q /. (j + 1)) by A19, AS, A21, A18, A8 .= (a * (fp . j)) + (a * (p /. (j + 1))) by AS, A20a .= a * ((fp . j) + (p /. (j + 1))) by VECTSP_1:def_2 .= a * (fp . (j + 1)) by A21a, A18, A14 ; hence S1[j + 1] ; ::_thesis: verum end; for j being Element of NAT st 0 <= j & j <= len p holds S1[j] from INT_1:sch_7(B1, B2); hence Sum q = a * (Sum p) by AS, A12, A6; ::_thesis: verum end; theorem del1a: :: RATFUNC1:2 for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr for f being FinSequence of L for i, j being Element of NAT st i in dom f & j = i - 1 holds Ins ((Del (f,i)),j,(f /. i)) = f proof let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for f being FinSequence of L for i, j being Element of NAT st i in dom f & j = i - 1 holds Ins ((Del (f,i)),j,(f /. i)) = f let f be FinSequence of L; ::_thesis: for i, j being Element of NAT st i in dom f & j = i - 1 holds Ins ((Del (f,i)),j,(f /. i)) = f let i, j be Element of NAT ; ::_thesis: ( i in dom f & j = i - 1 implies Ins ((Del (f,i)),j,(f /. i)) = f ) set g = Ins ((Del (f,i)),j,(f /. i)); assume AS: ( i in dom f & j = i - 1 ) ; ::_thesis: Ins ((Del (f,i)),j,(f /. i)) = f then consider n being Nat such that H0: ( len f = n + 1 & len (Del (f,i)) = n ) by FINSEQ_3:104; dom f = Seg (n + 1) by H0, FINSEQ_1:def_3; then consider ii being Element of NAT such that H1: ( i = ii & 1 <= ii & ii <= n + 1 ) by AS; i - 1 < i - 0 by XREAL_1:15; then j < n + 1 by AS, H1, XXREAL_0:2; then H2: j <= n by NAT_1:13; H3: len (Ins ((Del (f,i)),j,(f /. i))) = (len (Del (f,i))) + 1 by FINSEQ_5:69; now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(Ins_((Del_(f,i)),j,(f_/._i)))_holds_ (Ins_((Del_(f,i)),j,(f_/._i)))_._k_=_f_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len (Ins ((Del (f,i)),j,(f /. i))) implies (Ins ((Del (f,i)),j,(f /. i))) . k = f . k ) assume B: ( 1 <= k & k <= len (Ins ((Del (f,i)),j,(f /. i))) ) ; ::_thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k then k in Seg (len (Ins ((Del (f,i)),j,(f /. i)))) by FINSEQ_1:1; then D: k in dom (Ins ((Del (f,i)),j,(f /. i))) by FINSEQ_1:def_3; now__::_thesis:_(Ins_((Del_(f,i)),j,(f_/._i)))_._k_=_f_._k percases ( k < i or k = i or k > i ) by XXREAL_0:1; supposeC: k < i ; ::_thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k then k + 1 <= i by NAT_1:13; then (k + 1) - 1 <= i - 1 by XREAL_1:9; then ( 1 <= k & k <= len ((Del (f,i)) | j) ) by B, AS, H2, H0, FINSEQ_1:59; then k in Seg (len ((Del (f,i)) | j)) by FINSEQ_1:1; then D1: k in dom ((Del (f,i)) | j) by FINSEQ_1:def_3; k < n + 1 by H1, C, XXREAL_0:2; then k <= n by NAT_1:13; then k in Seg (len (Del (f,i))) by H0, B, FINSEQ_1:1; then D2: k in dom (Del (f,i)) by FINSEQ_1:def_3; (Ins ((Del (f,i)),j,(f /. i))) /. k = (Del (f,i)) /. k by D1, FINSEQ_5:72 .= (Del (f,i)) . k by D2, PARTFUN1:def_6 .= f . k by C, FINSEQ_3:110 ; hence (Ins ((Del (f,i)),j,(f /. i))) . k = f . k by D, PARTFUN1:def_6; ::_thesis: verum end; supposeC: k = i ; ::_thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k then k = j + 1 by AS; then E: (Ins ((Del (f,i)),j,(f /. i))) /. k = f /. i by H0, H2, FINSEQ_5:73; thus (Ins ((Del (f,i)),j,(f /. i))) . k = (Ins ((Del (f,i)),j,(f /. i))) /. k by D, PARTFUN1:def_6 .= f . k by AS, C, E, PARTFUN1:def_6 ; ::_thesis: verum end; supposeC: k > i ; ::_thesis: f . k = (Ins ((Del (f,i)),j,(f /. i))) . k then reconsider k1 = k - 1 as Element of NAT by H1, XXREAL_0:2, INT_1:5; C2: k - 1 <= (n + 1) - 1 by B, H0, H3, XREAL_1:9; 1 < k1 + 1 by C, H1, XXREAL_0:2; then 1 <= k1 by NAT_1:13; then k1 in Seg n by C2; then D1: k1 in dom (Del (f,i)) by H0, FINSEQ_1:def_3; i < k1 + 1 by C; then C1: j + 1 <= k - 1 by AS, NAT_1:13; then (Ins ((Del (f,i)),j,(f /. i))) /. (k1 + 1) = (Del (f,i)) /. k1 by C2, H0, FINSEQ_5:74 .= (Del (f,i)) . k1 by D1, PARTFUN1:def_6 .= f . (k1 + 1) by C1, C2, H0, AS, FINSEQ_3:111 ; hence f . k = (Ins ((Del (f,i)),j,(f /. i))) . k by D, PARTFUN1:def_6; ::_thesis: verum end; end; end; hence (Ins ((Del (f,i)),j,(f /. i))) . k = f . k ; ::_thesis: verum end; hence Ins ((Del (f,i)),j,(f /. i)) = f by H0, FINSEQ_5:69, FINSEQ_1:14; ::_thesis: verum end; theorem del1: :: RATFUNC1:3 for L being non empty right_complementable unital associative commutative right-distributive add-associative right_zeroed doubleLoopStr for f being FinSequence of L for i being Element of NAT st i in dom f holds Product f = (f /. i) * (Product (Del (f,i))) proof let L be non empty right_complementable unital associative commutative right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for f being FinSequence of L for i being Element of NAT st i in dom f holds Product f = (f /. i) * (Product (Del (f,i))) let f be FinSequence of L; ::_thesis: for i being Element of NAT st i in dom f holds Product f = (f /. i) * (Product (Del (f,i))) let i be Element of NAT ; ::_thesis: ( i in dom f implies Product f = (f /. i) * (Product (Del (f,i))) ) assume AS: i in dom f ; ::_thesis: Product f = (f /. i) * (Product (Del (f,i))) then i in Seg (len f) by FINSEQ_1:def_3; then consider ii being Element of NAT such that H: ( ii = i & 1 <= ii & ii <= len f ) ; reconsider j = i - 1 as Element of NAT by H, INT_1:5; set g = Del (f,i); thus Product f = Product (Ins ((Del (f,i)),j,(f /. i))) by AS, del1a .= (Product (((Del (f,i)) | j) ^ <*(f /. i)*>)) * (Product ((Del (f,i)) /^ j)) by GROUP_4:5 .= ((Product ((Del (f,i)) | j)) * (f /. i)) * (Product ((Del (f,i)) /^ j)) by GROUP_4:6 .= (f /. i) * ((Product ((Del (f,i)) | j)) * (Product ((Del (f,i)) /^ j))) by GROUP_1:def_3 .= (f /. i) * (Product (((Del (f,i)) | j) ^ ((Del (f,i)) /^ j))) by GROUP_4:5 .= (f /. i) * (Product (Del (f,i))) by RFINSEQ:8 ; ::_thesis: verum end; registration let L be non trivial right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed domRing-like doubleLoopStr ; let x, y be non zero Element of L; clusterx / y -> non zero ; coherence not x / y is zero proof ( x <> 0. L & y <> 0. L ) ; then (y ") * y = 1. L by VECTSP_1:def_10; then y " <> 0. L by VECTSP_1:7; hence x / y <> 0. L by VECTSP_2:def_1; :: according to STRUCT_0:def_12 ::_thesis: verum end; end; registration cluster non empty right_complementable right-distributive add-associative right_zeroed domRing-like -> non empty right_complementable almost_left_cancelable right-distributive add-associative right_zeroed for doubleLoopStr ; coherence for b1 being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr st b1 is domRing-like holds b1 is almost_left_cancelable proof let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: ( L is domRing-like implies L is almost_left_cancelable ) assume B: L is domRing-like ; ::_thesis: L is almost_left_cancelable let x be Element of L; :: according to ALGSTR_0:def_36 ::_thesis: ( x = 0. L or x is left_mult-cancelable ) assume A: x <> 0. L ; ::_thesis: x is left_mult-cancelable let y, z be Element of L; :: according to ALGSTR_0:def_20 ::_thesis: ( not x * y = x * z or y = z ) assume x * y = x * z ; ::_thesis: y = z then (x * y) - (x * z) = 0. L by RLVECT_1:15; then x * (y - z) = 0. L by VECTSP_1:11; then y - z = 0. L by A, B, VECTSP_2:def_1; hence y = z by RLVECT_1:21; ::_thesis: verum end; cluster non empty right_complementable left-distributive add-associative right_zeroed domRing-like -> non empty right_complementable almost_right_cancelable left-distributive add-associative right_zeroed for doubleLoopStr ; coherence for b1 being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr st b1 is domRing-like holds b1 is almost_right_cancelable proof let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: ( L is domRing-like implies L is almost_right_cancelable ) assume B: L is domRing-like ; ::_thesis: L is almost_right_cancelable let x be Element of L; :: according to ALGSTR_0:def_37 ::_thesis: ( x = 0. L or x is right_mult-cancelable ) assume A: x <> 0. L ; ::_thesis: x is right_mult-cancelable let y, z be Element of L; :: according to ALGSTR_0:def_21 ::_thesis: ( not y * x = z * x or y = z ) assume y * x = z * x ; ::_thesis: y = z then (y * x) - (z * x) = 0. L by RLVECT_1:15; then (y - z) * x = 0. L by VECTSP_1:13; then y - z = 0. L by A, B, VECTSP_2:def_1; hence y = z by RLVECT_1:21; ::_thesis: verum end; end; registration let x, y be Integer; cluster max (x,y) -> integer ; coherence max (x,y) is integer by XXREAL_0:16; cluster min (x,y) -> integer ; coherence min (x,y) is integer by XXREAL_0:15; end; theorem maxx: :: RATFUNC1:4 for x, y, z being Integer holds max ((x + y),(x + z)) = x + (max (y,z)) proof let x, y, z be Integer; ::_thesis: max ((x + y),(x + z)) = x + (max (y,z)) percases ( y <= z or y > z ) ; supposeA: y <= z ; ::_thesis: max ((x + y),(x + z)) = x + (max (y,z)) then x + y <= x + z by XREAL_1:6; hence max ((x + y),(x + z)) = x + z by XXREAL_0:def_10 .= x + (max (y,z)) by A, XXREAL_0:def_10 ; ::_thesis: verum end; supposeA: y > z ; ::_thesis: max ((x + y),(x + z)) = x + (max (y,z)) then x + y > x + z by XREAL_1:8; hence max ((x + y),(x + z)) = x + y by XXREAL_0:def_10 .= x + (max (y,z)) by A, XXREAL_0:def_10 ; ::_thesis: verum end; end; end; begin definition let L be non empty ZeroStr ; let p be Polynomial of L; attrp is zero means :defzer: :: RATFUNC1:def 1 p = 0_. L; attrp is constant means :defconst: :: RATFUNC1:def 2 deg p <= 0 ; end; :: deftheorem defzer defines zero RATFUNC1:def_1_:_ for L being non empty ZeroStr for p being Polynomial of L holds ( p is zero iff p = 0_. L ); :: deftheorem defconst defines constant RATFUNC1:def_2_:_ for L being non empty ZeroStr for p being Polynomial of L holds ( p is constant iff deg p <= 0 ); registration let L be non trivial ZeroStr ; clusterV1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support non zero for Element of K19(K20(NAT, the carrier of L)); existence not for b1 being Polynomial of L holds b1 is zero proof now__::_thesis:_ex_x_being_Element_of_the_carrier_of_L_st_x_<>_0._L assume AS: for x being Element of the carrier of L holds not x <> 0. L ; ::_thesis: contradiction now__::_thesis:_for_x,_y_being_Element_of_the_carrier_of_L_holds_y_=_x let x, y be Element of the carrier of L; ::_thesis: y = x thus y = 0. L by AS .= x by AS ; ::_thesis: verum end; hence contradiction by STRUCT_0:def_10; ::_thesis: verum end; then consider x being Element of the carrier of L such that C: x <> 0. L ; set p = (0_. L) +* (0,x); ex n being Nat st for i being Nat st i >= n holds ((0_. L) +* (0,x)) . i = 0. L proof take 1 ; ::_thesis: for i being Nat st i >= 1 holds ((0_. L) +* (0,x)) . i = 0. L now__::_thesis:_for_i_being_Nat_st_i_>=_1_holds_ ((0_._L)_+*_(0,x))_._i_=_0._L let i be Nat; ::_thesis: ( i >= 1 implies ((0_. L) +* (0,x)) . i = 0. L ) assume AS: i >= 1 ; ::_thesis: ((0_. L) +* (0,x)) . i = 0. L B: i in NAT by ORDINAL1:def_12; thus ((0_. L) +* (0,x)) . i = (0_. L) . i by AS, FUNCT_7:32 .= 0. L by B, FUNCOP_1:7 ; ::_thesis: verum end; hence for i being Nat st i >= 1 holds ((0_. L) +* (0,x)) . i = 0. L ; ::_thesis: verum end; then reconsider p = (0_. L) +* (0,x) as Polynomial of L by ALGSEQ_1:def_1; take p ; ::_thesis: not p is zero now__::_thesis:_for_i_being_Nat_st_i_<_1_holds_ p_._i_<>_0._L let i be Nat; ::_thesis: ( i < 1 implies p . i <> 0. L ) assume i < 1 ; ::_thesis: p . i <> 0. L then A: i = 0 by NAT_1:14; i in NAT by ORDINAL1:def_12; then 0 in dom (0_. L) by A, FUNCT_2:def_1; hence p . i <> 0. L by C, A, FUNCT_7:31; ::_thesis: verum end; then len p <> 0 by ALGSEQ_1:9; hence p <> 0_. L by POLYNOM4:3; :: according to RATFUNC1:def_1 ::_thesis: verum end; end; registration let L be non empty ZeroStr ; cluster 0_. L -> zero constant ; coherence ( 0_. L is zero & 0_. L is constant ) proof deg (0_. L) = - 1 by HURWITZ:20; hence ( 0_. L is zero & 0_. L is constant ) by defconst, defzer; ::_thesis: verum end; end; registration let L be non degenerated multLoopStr_0 ; cluster 1_. L -> non zero ; coherence not 1_. L is zero proof A: (1_. L) . 0 = 1. L by POLYNOM3:30; (0_. L) . 0 = 0. L by FUNCOP_1:7; hence not 1_. L is zero by defzer, A; ::_thesis: verum end; end; registration let L be non empty multLoopStr_0 ; cluster 1_. L -> constant ; coherence 1_. L is constant proof set p = 1_. L; now__::_thesis:_1_._L_is_constant percases ( 0. L = 1. L or 0. L <> 1. L ) ; supposeI: 0. L = 1. L ; ::_thesis: 1_. L is constant A: dom (1_. L) = NAT by FUNCT_2:def_1 .= dom (0_. L) by FUNCT_2:def_1 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(1_._L)_holds_ (1_._L)_._x_=_(0_._L)_._x let x be set ; ::_thesis: ( x in dom (1_. L) implies (1_. L) . x = (0_. L) . x ) assume x in dom (1_. L) ; ::_thesis: (1_. L) . x = (0_. L) . x then reconsider xx = x as Element of NAT ; B: (0_. L) . xx = 0. L by FUNCOP_1:7; ( xx = 0 or xx <> 0 ) ; hence (1_. L) . x = (0_. L) . x by I, B, POLYNOM3:30; ::_thesis: verum end; hence 1_. L is constant by A, FUNCT_1:2; ::_thesis: verum end; supposeI: 0. L <> 1. L ; ::_thesis: 1_. L is constant now__::_thesis:_for_i_being_Nat_st_i_>=_1_holds_ (1_._L)_._i_=_0._L let i be Nat; ::_thesis: ( i >= 1 implies (1_. L) . i = 0. L ) assume AS: i >= 1 ; ::_thesis: (1_. L) . i = 0. L B: i in NAT by ORDINAL1:def_12; thus (1_. L) . i = (0_. L) . i by AS, FUNCT_7:32 .= 0. L by B, FUNCOP_1:7 ; ::_thesis: verum end; then D: 1 is_at_least_length_of 1_. L by ALGSEQ_1:def_2; now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_1_._L_holds_ 1_<=_m let m be Nat; ::_thesis: ( m is_at_least_length_of 1_. L implies 1 <= m ) assume AS: m is_at_least_length_of 1_. L ; ::_thesis: 1 <= m now__::_thesis:_not_m_<_1 assume m < 1 ; ::_thesis: contradiction then m < 1 + 0 ; then m <= 0 by NAT_1:13; then E: (1_. L) . 0 = 0. L by AS, ALGSEQ_1:def_2; dom (0_. L) = NAT by FUNCOP_1:13; hence contradiction by I, E, FUNCT_7:31; ::_thesis: verum end; hence 1 <= m ; ::_thesis: verum end; then len (1_. L) = 1 by D, ALGSEQ_1:def_3; then deg (1_. L) = 0 ; hence 1_. L is constant by defconst; ::_thesis: verum end; end; end; hence 1_. L is constant ; ::_thesis: verum end; end; registration let L be non empty ZeroStr ; cluster Function-like V18( NAT , the carrier of L) finite-Support zero -> constant for Element of K19(K20(NAT, the carrier of L)); coherence for b1 being Polynomial of L st b1 is zero holds b1 is constant proof let p be Polynomial of L; ::_thesis: ( p is zero implies p is constant ) assume p is zero ; ::_thesis: p is constant then p = 0_. L by defzer; hence p is constant ; ::_thesis: verum end; end; registration let L be non empty ZeroStr ; cluster Function-like V18( NAT , the carrier of L) finite-Support non constant -> non zero for Element of K19(K20(NAT, the carrier of L)); coherence for b1 being Polynomial of L st not b1 is constant holds not b1 is zero ; end; registration let L be non trivial ZeroStr ; clusterV1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support non constant for Element of K19(K20(NAT, the carrier of L)); existence not for b1 being Polynomial of L holds b1 is constant proof now__::_thesis:_ex_x_being_Element_of_the_carrier_of_L_st_x_<>_0._L assume AS: for x being Element of the carrier of L holds not x <> 0. L ; ::_thesis: contradiction now__::_thesis:_for_x,_y_being_Element_of_the_carrier_of_L_holds_y_=_x let x, y be Element of the carrier of L; ::_thesis: y = x thus y = 0. L by AS .= x by AS ; ::_thesis: verum end; hence contradiction by STRUCT_0:def_10; ::_thesis: verum end; then consider x being Element of the carrier of L such that C: x <> 0. L ; set p = ((0_. L) +* (0,x)) +* (1,x); ex n being Nat st for i being Nat st i >= n holds (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L proof take 2 ; ::_thesis: for i being Nat st i >= 2 holds (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L now__::_thesis:_for_i_being_Nat_st_i_>=_2_holds_ (((0_._L)_+*_(0,x))_+*_(1,x))_._i_=_0._L let i be Nat; ::_thesis: ( i >= 2 implies (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L ) assume AS: i >= 2 ; ::_thesis: (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L then C: 1 <> i ; B: i in NAT by ORDINAL1:def_12; thus (((0_. L) +* (0,x)) +* (1,x)) . i = ((0_. L) +* (0,x)) . i by C, FUNCT_7:32 .= (0_. L) . i by AS, FUNCT_7:32 .= 0. L by B, FUNCOP_1:7 ; ::_thesis: verum end; hence for i being Nat st i >= 2 holds (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L ; ::_thesis: verum end; then reconsider p = ((0_. L) +* (0,x)) +* (1,x) as Polynomial of L by ALGSEQ_1:def_1; take p ; ::_thesis: not p is constant now__::_thesis:_for_i_being_Nat_st_i_>=_2_holds_ p_._i_=_0._L let i be Nat; ::_thesis: ( i >= 2 implies p . i = 0. L ) assume AS: i >= 2 ; ::_thesis: p . i = 0. L then C: 1 <> i ; B: i in NAT by ORDINAL1:def_12; thus p . i = ((0_. L) +* (0,x)) . i by C, FUNCT_7:32 .= (0_. L) . i by AS, FUNCT_7:32 .= 0. L by B, FUNCOP_1:7 ; ::_thesis: verum end; then D: 2 is_at_least_length_of p by ALGSEQ_1:def_2; now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_p_holds_ 2_<=_m let m be Nat; ::_thesis: ( m is_at_least_length_of p implies 2 <= m ) assume AS: m is_at_least_length_of p ; ::_thesis: 2 <= m now__::_thesis:_not_m_<_2 assume m < 2 ; ::_thesis: contradiction then m < 1 + 1 ; then m <= 1 by NAT_1:13; then E: p . 1 = 0. L by AS, ALGSEQ_1:def_2; dom (0_. L) = NAT by FUNCOP_1:13; then dom ((0_. L) +* (0,x)) = NAT by FUNCT_7:30; hence contradiction by C, E, FUNCT_7:31; ::_thesis: verum end; hence 2 <= m ; ::_thesis: verum end; then len p = 2 by D, ALGSEQ_1:def_3; then deg p = 1 ; hence not p is constant by defconst; ::_thesis: verum end; end; registration let L be non empty non degenerated well-unital doubleLoopStr ; let z be Element of L; let k be Element of NAT ; cluster rpoly (k,z) -> non zero ; coherence not rpoly (k,z) is zero proof deg (rpoly (k,z)) = k by HURWITZ:27; then rpoly (k,z) <> 0_. L by HURWITZ:20; hence not rpoly (k,z) is zero by defzer; ::_thesis: verum end; end; registration let L be non degenerated right_complementable distributive add-associative right_zeroed doubleLoopStr ; cluster Polynom-Ring L -> non degenerated ; coherence not Polynom-Ring L is degenerated proof set S = Polynom-Ring L; ( 0. (Polynom-Ring L) = 0_. L & 1. (Polynom-Ring L) = 1_. L ) by POLYNOM3:def_10; hence not Polynom-Ring L is degenerated by STRUCT_0:def_8; ::_thesis: verum end; end; registration let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; cluster Polynom-Ring L -> domRing-like ; coherence Polynom-Ring L is domRing-like proof set Q = Polynom-Ring L; let x, y be Element of (Polynom-Ring L); :: according to VECTSP_2:def_1 ::_thesis: ( not x * y = 0. (Polynom-Ring L) or x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) ) assume aa: x * y = 0. (Polynom-Ring L) ; ::_thesis: ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) ) assume AS: ( x <> 0. (Polynom-Ring L) & y <> 0. (Polynom-Ring L) ) ; ::_thesis: contradiction reconsider p = x as Polynomial of L by POLYNOM3:def_10; reconsider q = y as Polynomial of L by POLYNOM3:def_10; p <> 0_. L by AS, POLYNOM3:def_10; then reconsider p = p as non zero Polynomial of L by defzer; q <> 0_. L by AS, POLYNOM3:def_10; then reconsider q = q as non zero Polynomial of L by defzer; p <> 0_. L ; then deg p <> - 1 by HURWITZ:20; then Ap: len p <> 0 ; (len p) + 1 > 0 + 1 by Ap, XREAL_1:8; then Dp: len p >= 1 by NAT_1:13; then (len p) - 1 >= 1 - 1 by XREAL_1:9; then Cp: (len p) -' 1 = (len p) - 1 by XREAL_0:def_2; then reconsider lp = (len p) - 1 as Nat ; q <> 0_. L ; then deg q <> - 1 by HURWITZ:20; then Aq: len q <> 0 ; (len q) + 1 > 0 + 1 by Aq, XREAL_1:8; then Dq: len q >= 1 by NAT_1:13; then Eq: (len q) - 1 >= 1 - 1 by XREAL_1:9; then (len q) -' 1 = (len q) - 1 by XREAL_0:def_2; then reconsider lq = (len q) - 1 as Nat ; set m = ((len p) + (len q)) - 2; (len p) + (len q) >= 1 + 1 by Dp, Dq, XREAL_1:7; then ((len p) + (len q)) - 2 >= 2 - 2 by XREAL_1:9; then reconsider m = ((len p) + (len q)) - 2 as Element of NAT by INT_1:3; consider r being FinSequence of the carrier of L such that X: ( len r = m + 1 & (p *' q) . m = Sum r & ( for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((m + 1) -' k)) ) ) by POLYNOM3:def_9; ((((len p) + (len q)) - 2) + 1) - (len p) = lq ; then X1a: (m + 1) -' (len p) = lq by XREAL_0:def_2; X6: (len p) + 0 <= (len p) + ((len q) - 1) by Eq, XREAL_1:6; then len p in Seg (len r) by Dp, X; then X1: len p in dom r by FINSEQ_1:def_3; then X2: r . (len p) = (p . lp) * (q . lq) by X1a, Cp, X; X4: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_&_k_<>_len_p_holds_ r_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom r & k <> len p implies r . k = 0. L ) assume Y: ( k in dom r & k <> len p ) ; ::_thesis: r . k = 0. L now__::_thesis:_r_._k_=_0._L percases ( k > len p or k <= len p ) ; suppose k > len p ; ::_thesis: r . k = 0. L then k >= (len p) + 1 by NAT_1:13; then H: k - 1 >= ((len p) + 1) - 1 by XREAL_1:9; k -' 1 >= len p by H, XREAL_0:def_2; then p . (k -' 1) = 0. L by ALGSEQ_1:8; then (p . (k -' 1)) * (q . ((m + 1) -' k)) = 0. L by VECTSP_1:7; hence r . k = 0. L by Y, X; ::_thesis: verum end; supposeU: k <= len p ; ::_thesis: r . k = 0. L k < len p by Y, U, XXREAL_0:1; then (m + 1) - k > (m + 1) - (len p) by XREAL_1:10; then (m + 1) - k >= ((len q) - 1) + 1 by INT_1:7; then (m + 1) -' k >= len q by XREAL_0:def_2; then q . ((m + 1) -' k) = 0. L by ALGSEQ_1:8; then (p . (k -' 1)) * (q . ((m + 1) -' k)) = 0. L by VECTSP_1:6; hence r . k = 0. L by Y, X; ::_thesis: verum end; end; end; hence r . k = 0. L ; ::_thesis: verum end; X3: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_r_&_i_<>_len_p_holds_ r_/._i_=_0._L let i be Element of NAT ; ::_thesis: ( i in dom r & i <> len p implies r /. i = 0. L ) assume Y: ( i in dom r & i <> len p ) ; ::_thesis: r /. i = 0. L then i in Seg (len r) by FINSEQ_1:def_3; then ( 1 <= i & i <= len r ) by FINSEQ_1:1; hence r /. i = r . i by FINSEQ_4:15 .= 0. L by Y, X4 ; ::_thesis: verum end; X5: (p *' q) . m = r /. (len p) by X, X1, X3, POLYNOM2:3 .= (p . lp) * (q . lq) by X2, X6, Dp, X, FINSEQ_4:15 ; len p = lp + 1 ; then XX: p . lp <> 0. L by ALGSEQ_1:10; len q = lq + 1 ; then q . lq <> 0. L by ALGSEQ_1:10; then X6: (p *' q) . m <> 0. L by XX, X5, VECTSP_2:def_1; (0_. L) . m = 0. L by FUNCOP_1:7; then p *' q <> 0. (Polynom-Ring L) by X6, POLYNOM3:def_10; hence contradiction by aa, POLYNOM3:def_10; ::_thesis: verum end; end; theorem :: RATFUNC1:5 for L being non empty right_complementable associative right-distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L for a being Element of L holds (a * p) *' q = a * (p *' q) proof let L be non empty right_complementable associative right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for a being Element of L holds (a * p) *' q = a * (p *' q) let p, q be Polynomial of L; ::_thesis: for a being Element of L holds (a * p) *' q = a * (p *' q) let a be Element of L; ::_thesis: (a * p) *' q = a * (p *' q) set f = (a * p) *' q; set g = a * (p *' q); A: dom ((a * p) *' q) = NAT by FUNCT_2:def_1 .= dom (a * (p *' q)) by FUNCT_2:def_1 ; now__::_thesis:_for_i_being_set_st_i_in_dom_((a_*_p)_*'_q)_holds_ ((a_*_p)_*'_q)_._i_=_(a_*_(p_*'_q))_._i let i be set ; ::_thesis: ( i in dom ((a * p) *' q) implies ((a * p) *' q) . i = (a * (p *' q)) . i ) assume i in dom ((a * p) *' q) ; ::_thesis: ((a * p) *' q) . i = (a * (p *' q)) . i then reconsider n = i as Element of NAT ; consider fr being FinSequence of the carrier of L such that A1: ( len fr = n + 1 & ((a * p) *' q) . i = Sum fr & ( for k being Element of NAT st k in dom fr holds fr . k = ((a * p) . (k -' 1)) * (q . ((n + 1) -' k)) ) ) by POLYNOM3:def_9; consider fa being FinSequence of the carrier of L such that A2: ( len fa = n + 1 & (p *' q) . i = Sum fa & ( for k being Element of NAT st k in dom fa holds fa . k = (p . (k -' 1)) * (q . ((n + 1) -' k)) ) ) by POLYNOM3:def_9; Seg (len fa) = dom fr by A1, A2, FINSEQ_1:def_3; then A4: dom fa = dom fr by FINSEQ_1:def_3; A3: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_fa_holds_ fr_/._k_=_a_*_(fa_/._k) let k be Element of NAT ; ::_thesis: ( k in dom fa implies fr /. k = a * (fa /. k) ) assume A3a: k in dom fa ; ::_thesis: fr /. k = a * (fa /. k) then fa . k = fa /. k by PARTFUN1:def_6; then reconsider x = fa . k as Element of L ; thus fr /. k = fr . k by A3a, A4, PARTFUN1:def_6 .= ((a * p) . (k -' 1)) * (q . ((n + 1) -' k)) by A4, A3a, A1 .= (a * (p . (k -' 1))) * (q . ((n + 1) -' k)) by POLYNOM5:def_3 .= a * ((p . (k -' 1)) * (q . ((n + 1) -' k))) by GROUP_1:def_3 .= a * x by A3a, A2 .= a * (fa /. k) by A3a, PARTFUN1:def_6 ; ::_thesis: verum end; (a * (p *' q)) . n = a * (Sum fa) by A2, POLYNOM5:def_3 .= ((a * p) *' q) . n by A3, A2, A1, df ; hence ((a * p) *' q) . i = (a * (p *' q)) . i ; ::_thesis: verum end; hence (a * p) *' q = a * (p *' q) by A, FUNCT_1:2; ::_thesis: verum end; theorem :: RATFUNC1:6 for L being non empty right_complementable associative commutative right-distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L for a being Element of L holds p *' (a * q) = a * (p *' q) proof let L be non empty right_complementable associative commutative right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for a being Element of L holds p *' (a * q) = a * (p *' q) let p, q be Polynomial of L; ::_thesis: for a being Element of L holds p *' (a * q) = a * (p *' q) let a be Element of L; ::_thesis: p *' (a * q) = a * (p *' q) set f = p *' (a * q); set g = a * (p *' q); A: dom (p *' (a * q)) = NAT by FUNCT_2:def_1 .= dom (a * (p *' q)) by FUNCT_2:def_1 ; now__::_thesis:_for_i_being_set_st_i_in_dom_(p_*'_(a_*_q))_holds_ (p_*'_(a_*_q))_._i_=_(a_*_(p_*'_q))_._i let i be set ; ::_thesis: ( i in dom (p *' (a * q)) implies (p *' (a * q)) . i = (a * (p *' q)) . i ) assume i in dom (p *' (a * q)) ; ::_thesis: (p *' (a * q)) . i = (a * (p *' q)) . i then reconsider n = i as Element of NAT ; consider fr being FinSequence of the carrier of L such that A1: ( len fr = n + 1 & (p *' (a * q)) . i = Sum fr & ( for k being Element of NAT st k in dom fr holds fr . k = (p . (k -' 1)) * ((a * q) . ((n + 1) -' k)) ) ) by POLYNOM3:def_9; consider fa being FinSequence of the carrier of L such that A2: ( len fa = n + 1 & (p *' q) . i = Sum fa & ( for k being Element of NAT st k in dom fa holds fa . k = (p . (k -' 1)) * (q . ((n + 1) -' k)) ) ) by POLYNOM3:def_9; Seg (len fa) = dom fr by A1, A2, FINSEQ_1:def_3; then A4: dom fa = dom fr by FINSEQ_1:def_3; A3: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_fa_holds_ fr_/._k_=_a_*_(fa_/._k) let k be Element of NAT ; ::_thesis: ( k in dom fa implies fr /. k = a * (fa /. k) ) assume A3a: k in dom fa ; ::_thesis: fr /. k = a * (fa /. k) then fa . k = fa /. k by PARTFUN1:def_6; then reconsider x = fa . k as Element of L ; thus fr /. k = fr . k by A3a, A4, PARTFUN1:def_6 .= (p . (k -' 1)) * ((a * q) . ((n + 1) -' k)) by A4, A3a, A1 .= (p . (k -' 1)) * (a * (q . ((n + 1) -' k))) by POLYNOM5:def_3 .= a * ((p . (k -' 1)) * (q . ((n + 1) -' k))) by GROUP_1:def_3 .= a * x by A3a, A2 .= a * (fa /. k) by A3a, PARTFUN1:def_6 ; ::_thesis: verum end; (a * (p *' q)) . n = a * (Sum fa) by A2, POLYNOM5:def_3 .= (p *' (a * q)) . n by A3, df, A2, A1 ; hence (p *' (a * q)) . i = (a * (p *' q)) . i ; ::_thesis: verum end; hence p *' (a * q) = a * (p *' q) by A, FUNCT_1:2; ::_thesis: verum end; registration let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; let p be non zero Polynomial of L; let a be non zero Element of L; clustera * p -> non zero ; coherence not a * p is zero proof a <> 0. L ; then len (a * p) = len p by POLYNOM5:25; then a * p <> 0_. L by POLYNOM4:3, POLYNOM4:5; hence not a * p is zero by defzer; ::_thesis: verum end; end; registration let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; let p1, p2 be non zero Polynomial of L; clusterp1 *' p2 -> non zero ; coherence not p1 *' p2 is zero proof reconsider x1 = p1 as Element of (Polynom-Ring L) by POLYNOM3:def_10; reconsider x2 = p2 as Element of (Polynom-Ring L) by POLYNOM3:def_10; p1 <> 0_. L ; then A: x1 <> 0. (Polynom-Ring L) by POLYNOM3:def_10; p2 <> 0_. L ; then x2 <> 0. (Polynom-Ring L) by POLYNOM3:def_10; then x1 * x2 <> 0. (Polynom-Ring L) by A, VECTSP_2:def_1; then p1 *' p2 <> 0. (Polynom-Ring L) by POLYNOM3:def_10; then p1 *' p2 <> 0_. L by POLYNOM3:def_10; hence not p1 *' p2 is zero by defzer; ::_thesis: verum end; end; theorem thequiv1: :: RATFUNC1:7 for L being non trivial right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for p1, p2 being Polynomial of L for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds p1 = p2 proof let L be non trivial right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds p1 = p2 let p1, p2 be Polynomial of L; ::_thesis: for p3 being non zero Polynomial of L st p1 *' p3 = p2 *' p3 holds p1 = p2 let p3 be non zero Polynomial of L; ::_thesis: ( p1 *' p3 = p2 *' p3 implies p1 = p2 ) assume AS: p1 *' p3 = p2 *' p3 ; ::_thesis: p1 = p2 reconsider x1 = p1 as Element of (Polynom-Ring L) by POLYNOM3:def_10; reconsider x2 = p2 as Element of (Polynom-Ring L) by POLYNOM3:def_10; reconsider x3 = p3 as Element of (Polynom-Ring L) by POLYNOM3:def_10; p3 <> 0_. L ; then A: x3 <> 0. (Polynom-Ring L) by POLYNOM3:def_10; B: x1 * x3 = p2 *' p3 by AS, POLYNOM3:def_10 .= x2 * x3 by POLYNOM3:def_10 ; x3 is right_mult-cancelable by A, ALGSTR_0:def_37; hence p1 = p2 by B, ALGSTR_0:def_21; ::_thesis: verum end; registration let L be non trivial ZeroStr ; let p be non zero Polynomial of L; cluster degree p -> natural ; coherence degree p is natural proof p <> 0_. L ; then deg p <> - 1 by HURWITZ:20; then len p <> 0 ; then (deg p) + 1 > 0 ; then deg p in NAT by INT_1:7, INT_1:3; hence degree p is natural ; ::_thesis: verum end; end; theorem degrat2: :: RATFUNC1:8 for L being non empty right_complementable unital right-distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L st deg p = 0 holds for x being Element of L holds eval (p,x) <> 0. L proof let L be non empty right_complementable unital right-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L st deg p = 0 holds for x being Element of L holds eval (p,x) <> 0. L let p be Polynomial of L; ::_thesis: ( deg p = 0 implies for x being Element of L holds eval (p,x) <> 0. L ) assume AS: deg p = 0 ; ::_thesis: for x being Element of L holds eval (p,x) <> 0. L let x be Element of L; ::_thesis: eval (p,x) <> 0. L assume eval (p,x) = 0. L ; ::_thesis: contradiction then x is_a_root_of p by POLYNOM5:def_6; then p is with_roots by POLYNOM5:def_7; hence contradiction by AS, HURWITZ:24; ::_thesis: verum end; theorem div1: :: RATFUNC1:9 for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for p being Polynomial of L for x being Element of L holds ( eval (p,x) = 0. L iff rpoly (1,x) divides p ) proof let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for x being Element of L holds ( eval (p,x) = 0. L iff rpoly (1,x) divides p ) let p be Polynomial of L; ::_thesis: for x being Element of L holds ( eval (p,x) = 0. L iff rpoly (1,x) divides p ) let x be Element of L; ::_thesis: ( eval (p,x) = 0. L iff rpoly (1,x) divides p ) A: now__::_thesis:_(_rpoly_(1,x)_divides_p_implies_eval_(p,x)_=_0._L_) assume rpoly (1,x) divides p ; ::_thesis: eval (p,x) = 0. L then p mod (rpoly (1,x)) = 0_. L by HURWITZ:def_7; then (p - ((p div (rpoly (1,x))) *' (rpoly (1,x)))) + ((p div (rpoly (1,x))) *' (rpoly (1,x))) = (p div (rpoly (1,x))) *' (rpoly (1,x)) by POLYNOM3:28; then B: (p div (rpoly (1,x))) *' (rpoly (1,x)) = p + ((- ((p div (rpoly (1,x))) *' (rpoly (1,x)))) + ((p div (rpoly (1,x))) *' (rpoly (1,x)))) by POLYNOM3:26 .= p + (((p div (rpoly (1,x))) *' (rpoly (1,x))) - ((p div (rpoly (1,x))) *' (rpoly (1,x)))) .= p + (0_. L) by POLYNOM3:29 .= p by POLYNOM3:28 ; C: eval ((rpoly (1,x)),x) = x - x by HURWITZ:29 .= 0. L by RLVECT_1:15 ; thus eval (p,x) = (eval ((p div (rpoly (1,x))),x)) * (0. L) by C, B, POLYNOM4:24 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; ( eval (p,x) = 0. L implies rpoly (1,x) divides p ) by HURWITZ:35, POLYNOM5:def_6; hence ( eval (p,x) = 0. L iff rpoly (1,x) divides p ) by A; ::_thesis: verum end; theorem div3: :: RATFUNC1:10 for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for p, q being Polynomial of L for x being Element of L holds ( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q ) proof let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for x being Element of L holds ( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q ) let p, q be Polynomial of L; ::_thesis: for x being Element of L holds ( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q ) let x be Element of L; ::_thesis: ( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q ) assume rpoly (1,x) divides p *' q ; ::_thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q ) then eval ((p *' q),x) = 0. L by div1; then A: (eval (p,x)) * (eval (q,x)) = 0. L by POLYNOM4:24; percases ( eval (p,x) = 0. L or eval (q,x) = 0. L ) by A, VECTSP_2:def_1; suppose eval (p,x) = 0. L ; ::_thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q ) hence ( rpoly (1,x) divides p or rpoly (1,x) divides q ) by div1; ::_thesis: verum end; suppose eval (q,x) = 0. L ; ::_thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q ) hence ( rpoly (1,x) divides p or rpoly (1,x) divides q ) by div1; ::_thesis: verum end; end; end; theorem div4: :: RATFUNC1:11 for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) holds for p being Polynomial of L st p = Product f holds p <> 0_. L proof let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) holds for p being Polynomial of L st p = Product f holds p <> 0_. L let f be FinSequence of (Polynom-Ring L); ::_thesis: ( ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds p <> 0_. L ) assume AS1: for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ; ::_thesis: for p being Polynomial of L st p = Product f holds p <> 0_. L let p be Polynomial of L; ::_thesis: ( p = Product f implies p <> 0_. L ) assume AS2: p = Product f ; ::_thesis: p <> 0_. L defpred S1[ Nat] means for f being FinSequence of (Polynom-Ring L) st len f = $1 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) holds for p being Polynomial of L st p = Product f holds p <> 0_. L; now__::_thesis:_for_f_being_FinSequence_of_(Polynom-Ring_L)_st_len_f_=_0_&_(_for_i_being_Nat_st_i_in_dom_f_holds_ ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)_)_holds_ for_p_being_Polynomial_of_L_st_p_=_Product_f_holds_ p_<>_0_._L let f be FinSequence of (Polynom-Ring L); ::_thesis: ( len f = 0 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds p <> 0_. L ) assume A1: ( len f = 0 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) ) ; ::_thesis: for p being Polynomial of L st p = Product f holds p <> 0_. L let p be Polynomial of L; ::_thesis: ( p = Product f implies p <> 0_. L ) assume A2: p = Product f ; ::_thesis: p <> 0_. L f = <*> the carrier of (Polynom-Ring L) by A1; then p = 1_ (Polynom-Ring L) by A2, GROUP_4:8 .= 1. (Polynom-Ring L) ; then p <> 0. (Polynom-Ring L) ; hence p <> 0_. L by POLYNOM3:def_10; ::_thesis: verum end; then IA: S1[ 0 ] ; IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume IV: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_f_being_FinSequence_of_(Polynom-Ring_L)_st_len_f_=_n_+_1_&_(_for_i_being_Nat_st_i_in_dom_f_holds_ ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)_)_holds_ for_p_being_Polynomial_of_L_st_p_=_Product_f_holds_ p_<>_0_._L let f be FinSequence of (Polynom-Ring L); ::_thesis: ( len f = n + 1 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds p <> 0_. L ) assume A1: ( len f = n + 1 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) ) ; ::_thesis: for p being Polynomial of L st p = Product f holds p <> 0_. L let p be Polynomial of L; ::_thesis: ( p = Product f implies p <> 0_. L ) assume A2: p = Product f ; ::_thesis: p <> 0_. L f <> {} by A1; then consider g being FinSequence, u being set such that A6: f = g ^ <*u*> by FINSEQ_1:46; reconsider g = g as FinSequence of (Polynom-Ring L) by A6, FINSEQ_1:36; A2c: dom f = Seg (n + 1) by A1, FINSEQ_1:def_3; 1 <= n + 1 by NAT_1:11; then A2a: n + 1 in dom f by A2c; A2c: n + 1 = (len g) + (len <*u*>) by A1, A6, FINSEQ_1:22 .= (len g) + 1 by FINSEQ_1:40 ; then f . (n + 1) = u by A6, FINSEQ_1:42; then consider z being Element of L such that U: u = rpoly (1,z) by A1, A2a; reconsider u = u as Element of (Polynom-Ring L) by U, POLYNOM3:def_10; reconsider q = Product g as Polynomial of L by POLYNOM3:def_10; A4: Product f = (Product g) * u by A6, GROUP_4:6; A3: u <> 0. (Polynom-Ring L) by U, POLYNOM3:def_10; now__::_thesis:_for_i_being_Nat_st_i_in_dom_g_holds_ ex_z_being_Element_of_L_st_g_._i_=_rpoly_(1,z) let i be Nat; ::_thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) ) assume G: i in dom g ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z) then H: g . i = f . i by A6, FINSEQ_1:def_7; dom g c= dom f by A6, FINSEQ_1:26; hence ex z being Element of L st g . i = rpoly (1,z) by G, H, A1; ::_thesis: verum end; then q <> 0_. L by IV, A2c; then q <> 0. (Polynom-Ring L) by POLYNOM3:def_10; then p <> 0. (Polynom-Ring L) by A2, A3, A4, VECTSP_2:def_1; hence p <> 0_. L by POLYNOM3:def_10; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS); len f is Nat ; hence p <> 0_. L by AS1, AS2, I; ::_thesis: verum end; theorem div2: :: RATFUNC1:12 for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) holds for p being Polynomial of L st p = Product f holds for x being Element of L holds ( eval (p,x) = 0. L iff ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) proof let L be Field; ::_thesis: for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) holds for p being Polynomial of L st p = Product f holds for x being Element of L holds ( eval (p,x) = 0. L iff ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) let f be FinSequence of (Polynom-Ring L); ::_thesis: ( ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds for x being Element of L holds ( eval (p,x) = 0. L iff ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) ) assume AS1: for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ; ::_thesis: for p being Polynomial of L st p = Product f holds for x being Element of L holds ( eval (p,x) = 0. L iff ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) let p be Polynomial of L; ::_thesis: ( p = Product f implies for x being Element of L holds ( eval (p,x) = 0. L iff ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) ) assume AS2: p = Product f ; ::_thesis: for x being Element of L holds ( eval (p,x) = 0. L iff ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) let x be Element of L; ::_thesis: ( eval (p,x) = 0. L iff ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) A: now__::_thesis:_(_ex_i_being_Nat_st_ (_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)_implies_eval_(p,x)_=_0._L_) assume ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ; ::_thesis: eval (p,x) = 0. L then consider i being Nat such that A1: ( i in dom f & f . i = rpoly (1,x) ) ; reconsider g = Del (f,i) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105; reconsider q = Product g as Polynomial of L by POLYNOM3:def_10; A2: f /. i = rpoly (1,x) by A1, PARTFUN1:def_6; Product f = (f /. i) * (Product g) by A1, del1; then p = (rpoly (1,x)) *' q by AS2, A2, POLYNOM3:def_10; then A3: eval (p,x) = (eval ((rpoly (1,x)),x)) * (eval (q,x)) by POLYNOM4:24; eval ((rpoly (1,x)),x) = x - x by HURWITZ:29 .= 0. L by RLVECT_1:15 ; hence eval (p,x) = 0. L by A3, VECTSP_1:7; ::_thesis: verum end; now__::_thesis:_(_eval_(p,x)_=_0._L_implies_ex_i_being_Nat_st_ (_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)_) assume A0: eval (p,x) = 0. L ; ::_thesis: ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) defpred S1[ Nat] means for f being FinSequence of (Polynom-Ring L) st len f = $1 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) holds for p being Polynomial of L st p = Product f holds for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ); now__::_thesis:_for_f_being_FinSequence_of_(Polynom-Ring_L)_st_len_f_=_0_&_(_for_i_being_Nat_st_i_in_dom_f_holds_ ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)_)_holds_ for_p_being_Polynomial_of_L_st_p_=_Product_f_holds_ for_x_being_Element_of_L_st_eval_(p,x)_=_0._L_holds_ ex_i_being_Nat_st_ (_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_) let f be FinSequence of (Polynom-Ring L); ::_thesis: ( len f = 0 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) assume A1: ( len f = 0 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) ) ; ::_thesis: for p being Polynomial of L st p = Product f holds for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) let p be Polynomial of L; ::_thesis: ( p = Product f implies for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) assume A2: p = Product f ; ::_thesis: for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) let x be Element of L; ::_thesis: ( eval (p,x) = 0. L implies ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) assume A3: eval (p,x) = 0. L ; ::_thesis: ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) f = <*> the carrier of (Polynom-Ring L) by A1; then p = 1_ (Polynom-Ring L) by A2, GROUP_4:8 .= 1_. L by POLYNOM3:def_10 ; hence ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) by A3, POLYNOM4:18; ::_thesis: verum end; then IA: S1[ 0 ] ; IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume IV: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_f_being_FinSequence_of_(Polynom-Ring_L)_st_len_f_=_n_+_1_&_(_for_i_being_Nat_st_i_in_dom_f_holds_ ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z)_)_holds_ for_p_being_Polynomial_of_L_st_p_=_Product_f_holds_ for_x_being_Element_of_L_st_eval_(p,x)_=_0._L_holds_ ex_i_being_Nat_st_ (_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_) let f be FinSequence of (Polynom-Ring L); ::_thesis: ( len f = n + 1 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) assume A1: ( len f = n + 1 & ( for i being Nat st i in dom f holds ex z being Element of L st f . i = rpoly (1,z) ) ) ; ::_thesis: for p being Polynomial of L st p = Product f holds for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) let p be Polynomial of L; ::_thesis: ( p = Product f implies for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) assume A2: p = Product f ; ::_thesis: for x being Element of L st eval (p,x) = 0. L holds ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) let x be Element of L; ::_thesis: ( eval (p,x) = 0. L implies ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) assume A3: eval (p,x) = 0. L ; ::_thesis: ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) f <> {} by A1; then consider g being FinSequence, u being set such that A6: f = g ^ <*u*> by FINSEQ_1:46; reconsider g = g as FinSequence of (Polynom-Ring L) by A6, FINSEQ_1:36; A2c: dom f = Seg (n + 1) by A1, FINSEQ_1:def_3; 1 <= n + 1 by NAT_1:11; then A2a: n + 1 in dom f by A2c; A2c: n + 1 = (len g) + (len <*u*>) by A1, A6, FINSEQ_1:22 .= (len g) + 1 by FINSEQ_1:40 ; A2b: f . (n + 1) = u by A2c, A6, FINSEQ_1:42; then consider z being Element of L such that U: u = rpoly (1,z) by A1, A2a; reconsider u = u as Element of (Polynom-Ring L) by U, POLYNOM3:def_10; reconsider q = Product g as Polynomial of L by POLYNOM3:def_10; Product f = (Product g) * u by A6, GROUP_4:6 .= q *' (rpoly (1,z)) by U, POLYNOM3:def_10 ; then A4: eval (p,x) = (eval (q,x)) * (eval ((rpoly (1,z)),x)) by A2, POLYNOM4:24; A10: now__::_thesis:_for_i_being_Nat_st_i_in_dom_g_holds_ ex_z_being_Element_of_L_st_g_._i_=_rpoly_(1,z) let i be Nat; ::_thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) ) assume C1: i in dom g ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z) C2: dom g c= dom f by A6, FINSEQ_1:26; g . i = f . i by C1, A6, FINSEQ_1:def_7; hence ex z being Element of L st g . i = rpoly (1,z) by C1, C2, A1; ::_thesis: verum end; now__::_thesis:_ex_i_being_Nat_st_ (_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_) percases ( eval (q,x) = 0. L or eval ((rpoly (1,z)),x) = 0. L ) by A4, A3, VECTSP_2:def_1; suppose eval (q,x) = 0. L ; ::_thesis: ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) then consider i being Nat such that B1: ( i in dom g & g . i = rpoly (1,x) ) by A2c, A10, IV; B2: dom g c= dom f by A6, FINSEQ_1:26; f . i = rpoly (1,x) by B1, A6, FINSEQ_1:def_7; hence ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) by B2, B1; ::_thesis: verum end; suppose eval ((rpoly (1,z)),x) = 0. L ; ::_thesis: ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) then x - z = 0. L by HURWITZ:29; then x = z by RLVECT_1:21; hence ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) by A2a, A2b, U; ::_thesis: verum end; end; end; hence ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS); len f is Nat ; hence ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) by A0, AS1, AS2, I; ::_thesis: verum end; hence ( eval (p,x) = 0. L iff ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ) by A; ::_thesis: verum end; begin definition let L be non empty unital doubleLoopStr ; let p1, p2 be Polynomial of L; let x be Element of L; predx is_a_common_root_of p1,p2 means :root1: :: RATFUNC1:def 3 ( x is_a_root_of p1 & x is_a_root_of p2 ); end; :: deftheorem root1 defines is_a_common_root_of RATFUNC1:def_3_:_ for L being non empty unital doubleLoopStr for p1, p2 being Polynomial of L for x being Element of L holds ( x is_a_common_root_of p1,p2 iff ( x is_a_root_of p1 & x is_a_root_of p2 ) ); definition let L be non empty unital doubleLoopStr ; let p1, p2 be Polynomial of L; predp1,p2 have_a_common_root means :root2: :: RATFUNC1:def 4 ex x being Element of L st x is_a_common_root_of p1,p2; end; :: deftheorem root2 defines have_a_common_root RATFUNC1:def_4_:_ for L being non empty unital doubleLoopStr for p1, p2 being Polynomial of L holds ( p1,p2 have_a_common_root iff ex x being Element of L st x is_a_common_root_of p1,p2 ); notation let L be non empty unital doubleLoopStr ; let p1, p2 be Polynomial of L; synonym p1,p2 have_common_roots for p1,p2 have_a_common_root ; antonym p1,p2 have_no_common_roots for p1,p2 have_a_common_root ; end; theorem root3: :: RATFUNC1:13 for L being non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr for p being Polynomial of L for x being Element of L st x is_a_root_of p holds x is_a_root_of - p proof let L be non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for x being Element of L st x is_a_root_of p holds x is_a_root_of - p let p be Polynomial of L; ::_thesis: for x being Element of L st x is_a_root_of p holds x is_a_root_of - p let x be Element of L; ::_thesis: ( x is_a_root_of p implies x is_a_root_of - p ) assume AS: x is_a_root_of p ; ::_thesis: x is_a_root_of - p eval ((- p),x) = - (eval (p,x)) by POLYNOM4:20 .= - (0. L) by AS, POLYNOM5:def_6 .= 0. L by RLVECT_1:12 ; hence x is_a_root_of - p by POLYNOM5:def_6; ::_thesis: verum end; theorem root4: :: RATFUNC1:14 for L being non empty right_complementable unital left-distributive Abelian add-associative right_zeroed doubleLoopStr for p1, p2 being Polynomial of L for x being Element of L st x is_a_common_root_of p1,p2 holds x is_a_root_of p1 + p2 proof let L be non empty right_complementable unital left-distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L for x being Element of L st x is_a_common_root_of p1,p2 holds x is_a_root_of p1 + p2 let p1, p2 be Polynomial of L; ::_thesis: for x being Element of L st x is_a_common_root_of p1,p2 holds x is_a_root_of p1 + p2 let x be Element of L; ::_thesis: ( x is_a_common_root_of p1,p2 implies x is_a_root_of p1 + p2 ) assume x is_a_common_root_of p1,p2 ; ::_thesis: x is_a_root_of p1 + p2 then ( x is_a_root_of p1 & x is_a_root_of p2 ) by root1; then AS: ( eval (p1,x) = 0. L & eval (p2,x) = 0. L ) by POLYNOM5:def_6; eval ((p1 + p2),x) = (0. L) + (0. L) by AS, POLYNOM4:19 .= 0. L by RLVECT_1:def_4 ; hence x is_a_root_of p1 + p2 by POLYNOM5:def_6; ::_thesis: verum end; theorem :: RATFUNC1:15 for L being non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr for p1, p2 being Polynomial of L for x being Element of L st x is_a_common_root_of p1,p2 holds x is_a_root_of - (p1 + p2) by root3, root4; theorem :: RATFUNC1:16 for L being non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L for x being Element of L st x is_a_common_root_of p,q holds x is_a_root_of p + q proof let L be non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for x being Element of L st x is_a_common_root_of p,q holds x is_a_root_of p + q let p, q be Polynomial of L; ::_thesis: for x being Element of L st x is_a_common_root_of p,q holds x is_a_root_of p + q let x be Element of L; ::_thesis: ( x is_a_common_root_of p,q implies x is_a_root_of p + q ) assume x is_a_common_root_of p,q ; ::_thesis: x is_a_root_of p + q then H: ( x is_a_root_of p & x is_a_root_of q ) by root1; then H1: eval (p,x) = 0. L by POLYNOM5:def_6; H2: eval (q,x) = 0. L by H, POLYNOM5:def_6; eval ((p + q),x) = (0. L) + (0. L) by H1, H2, POLYNOM4:19 .= 0. L by RLVECT_1:def_4 ; hence x is_a_root_of p + q by POLYNOM5:def_6; ::_thesis: verum end; theorem :: RATFUNC1:17 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for p1, p2 being Polynomial of L st p1 divides p2 & p1 is with_roots holds p1,p2 have_common_roots proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L st p1 divides p2 & p1 is with_roots holds p1,p2 have_common_roots let p1, p2 be Polynomial of L; ::_thesis: ( p1 divides p2 & p1 is with_roots implies p1,p2 have_common_roots ) assume AS: ( p1 divides p2 & p1 is with_roots ) ; ::_thesis: p1,p2 have_common_roots percases ( p1 = 0_. L or p1 <> 0_. L ) ; supposeA: p1 = 0_. L ; ::_thesis: p1,p2 have_common_roots p2 mod p1 = 0_. L by AS, HURWITZ:def_7; then 0_. L = p2 - (0_. L) by A, POLYNOM3:34 .= p2 + (0_. L) by HURWITZ:9 ; then B: p2 = 0_. L by POLYNOM3:28; eval ((0_. L),(0. L)) = 0. L by POLYNOM4:17; then 0. L is_a_root_of 0_. L by POLYNOM5:def_6; then 0. L is_a_common_root_of p1,p2 by A, B, root1; hence p1,p2 have_common_roots by root2; ::_thesis: verum end; suppose p1 <> 0_. L ; ::_thesis: p1,p2 have_common_roots then consider s being Polynomial of L such that A: s *' p1 = p2 by AS, HURWITZ:34; consider x being Element of L such that B: x is_a_root_of p1 by AS, POLYNOM5:def_7; C: eval (p1,x) = 0. L by B, POLYNOM5:def_6; eval (p2,x) = (eval (s,x)) * (eval (p1,x)) by A, POLYNOM4:24 .= 0. L by C, VECTSP_1:6 ; then x is_a_root_of p2 by POLYNOM5:def_6; then x is_a_common_root_of p1,p2 by B, root1; hence p1,p2 have_common_roots by root2; ::_thesis: verum end; end; end; definition let L be non empty unital doubleLoopStr ; let p, q be Polynomial of L; func Common_Roots (p,q) -> Subset of L equals :: RATFUNC1:def 5 { x where x is Element of L : x is_a_common_root_of p,q } ; coherence { x where x is Element of L : x is_a_common_root_of p,q } is Subset of L proof set M = { x where x is Element of L : x is_a_common_root_of p,q } ; now__::_thesis:_for_u_being_set_st_u_in__{__x_where_x_is_Element_of_L_:_x_is_a_common_root_of_p,q__}__holds_ u_in_the_carrier_of_L let u be set ; ::_thesis: ( u in { x where x is Element of L : x is_a_common_root_of p,q } implies u in the carrier of L ) assume u in { x where x is Element of L : x is_a_common_root_of p,q } ; ::_thesis: u in the carrier of L then ex x being Element of L st ( u = x & x is_a_common_root_of p,q ) ; hence u in the carrier of L ; ::_thesis: verum end; hence { x where x is Element of L : x is_a_common_root_of p,q } is Subset of L by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines Common_Roots RATFUNC1:def_5_:_ for L being non empty unital doubleLoopStr for p, q being Polynomial of L holds Common_Roots (p,q) = { x where x is Element of L : x is_a_common_root_of p,q } ; begin definition let L be non empty ZeroStr ; let p be Polynomial of L; func Leading-Coefficient p -> Element of L equals :: RATFUNC1:def 6 p . ((len p) -' 1); coherence p . ((len p) -' 1) is Element of L ; end; :: deftheorem defines Leading-Coefficient RATFUNC1:def_6_:_ for L being non empty ZeroStr for p being Polynomial of L holds Leading-Coefficient p = p . ((len p) -' 1); notation let L be non empty ZeroStr ; let p be Polynomial of L; synonym LC p for Leading-Coefficient p; end; registration let L be non trivial doubleLoopStr ; let p be non zero Polynomial of L; cluster Leading-Coefficient p -> non zero ; coherence not LC p is zero proof p <> 0_. L ; then len p <> 0 by POLYNOM4:5; then 0 + 1 < (len p) + 1 by XREAL_1:8; then len p >= 1 by NAT_1:13; then ((len p) -' 1) + 1 = len p by XREAL_1:235; then p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10; hence not LC p is zero by STRUCT_0:def_12; ::_thesis: verum end; end; theorem lcp1: :: RATFUNC1:18 for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L for a being Element of L holds LC (a * p) = a * (LC p) proof let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Polynomial of L for a being Element of L holds LC (a * p) = a * (LC p) let p be Polynomial of L; ::_thesis: for a being Element of L holds LC (a * p) = a * (LC p) let a be Element of L; ::_thesis: LC (a * p) = a * (LC p) percases ( a = 0. L or a <> 0. L ) ; supposeA: a = 0. L ; ::_thesis: LC (a * p) = a * (LC p) then B: a * (LC p) = 0. L by VECTSP_1:6; a * p = 0_. L by A, POLYNOM5:26; hence LC (a * p) = a * (LC p) by B, FUNCOP_1:7; ::_thesis: verum end; supposeA: a <> 0. L ; ::_thesis: LC (a * p) = a * (LC p) thus LC (a * p) = a * (p . ((len (a * p)) -' 1)) by POLYNOM5:def_3 .= a * (LC p) by A, POLYNOM5:25 ; ::_thesis: verum end; end; end; definition let L be non empty doubleLoopStr ; let p be Polynomial of L; attrp is normalized means :defnormp: :: RATFUNC1:def 7 LC p = 1. L; end; :: deftheorem defnormp defines normalized RATFUNC1:def_7_:_ for L being non empty doubleLoopStr for p being Polynomial of L holds ( p is normalized iff LC p = 1. L ); registration let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; let p be non zero Polynomial of L; cluster((1. L) / (LC p)) * p -> normalized ; coherence ((1. L) / (LC p)) * p is normalized proof A: LC p <> 0. L ; LC (((1. L) / (LC p)) * p) = ((1. L) / (LC p)) * (LC p) by lcp1 .= (1. L) * (((LC p) ") * (LC p)) by GROUP_1:def_3 .= (1. L) * (1. L) by A, VECTSP_1:def_10 .= 1. L by VECTSP_1:def_4 ; hence ((1. L) / (LC p)) * p is normalized by defnormp; ::_thesis: verum end; end; registration let L be Field; let p be non zero Polynomial of L; cluster NormPolynomial p -> normalized ; coherence NormPolynomial p is normalized proof set q = NormPolynomial p; A: p <> 0_. L ; then (NormPolynomial p) . ((len p) -' 1) = 1. L by POLYNOM5:56, POLYNOM4:5; then LC (NormPolynomial p) = 1. L by A, POLYNOM5:57, POLYNOM4:5; hence NormPolynomial p is normalized by defnormp; ::_thesis: verum end; end; begin definition let L be non trivial multLoopStr_0 ; mode rational_function of L -> set means :defratf: :: RATFUNC1:def 8 ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st it = [p1,p2]; existence ex b1 being set ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b1 = [p1,p2] proof take [ the Polynomial of L, the non zero Polynomial of L] ; ::_thesis: ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st [ the Polynomial of L, the non zero Polynomial of L] = [p1,p2] thus ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st [ the Polynomial of L, the non zero Polynomial of L] = [p1,p2] ; ::_thesis: verum end; end; :: deftheorem defratf defines rational_function RATFUNC1:def_8_:_ for L being non trivial multLoopStr_0 for b2 being set holds ( b2 is rational_function of L iff ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st b2 = [p1,p2] ); definition let L be non trivial multLoopStr_0 ; let p1 be Polynomial of L; let p2 be non zero Polynomial of L; :: original: [ redefine func[p1,p2] -> rational_function of L; coherence [p1,p2] is rational_function of L by defratf; end; definition let L be non trivial multLoopStr_0 ; let z be rational_function of L; :: original: `1 redefine funcz `1 -> Polynomial of L; coherence z `1 is Polynomial of L proof consider p1 being Polynomial of L such that H: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf; consider p2 being non zero Polynomial of L such that H1: z = [p1,p2] by H; thus z `1 is Polynomial of L by H1, XTUPLE_0:def_2; ::_thesis: verum end; :: original: `2 redefine funcz `2 -> non zero Polynomial of L; coherence z `2 is non zero Polynomial of L proof consider p1 being Polynomial of L such that H: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf; consider p2 being non zero Polynomial of L such that H1: z = [p1,p2] by H; thus z `2 is non zero Polynomial of L by H1, XTUPLE_0:def_3; ::_thesis: verum end; end; definition let L be non trivial multLoopStr_0 ; let z be rational_function of L; attrz is zero means :defzerrat: :: RATFUNC1:def 9 z `1 = 0_. L; end; :: deftheorem defzerrat defines zero RATFUNC1:def_9_:_ for L being non trivial multLoopStr_0 for z being rational_function of L holds ( z is zero iff z `1 = 0_. L ); registration let L be non trivial multLoopStr_0 ; cluster non zero for rational_function of L; existence not for b1 being rational_function of L holds b1 is zero proof set p1 = the non zero Polynomial of L; set p2 = the non zero Polynomial of L; take [ the non zero Polynomial of L, the non zero Polynomial of L] ; ::_thesis: not [ the non zero Polynomial of L, the non zero Polynomial of L] is zero H: the non zero Polynomial of L = [ the non zero Polynomial of L, the non zero Polynomial of L] `1 ; the non zero Polynomial of L <> 0_. L ; hence not [ the non zero Polynomial of L, the non zero Polynomial of L] is zero by H, defzerrat; ::_thesis: verum end; end; theorem ttt: :: RATFUNC1:19 for L being non trivial multLoopStr_0 for z being rational_function of L holds z = [(z `1),(z `2)] proof let L be non trivial multLoopStr_0 ; ::_thesis: for z being rational_function of L holds z = [(z `1),(z `2)] let z be rational_function of L; ::_thesis: z = [(z `1),(z `2)] consider p1 being Polynomial of L such that H1: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf; consider p2 being non zero Polynomial of L such that H2: z = [p1,p2] by H1; ( z `1 = p1 & z `2 = p2 ) by H2, XTUPLE_0:def_2, XTUPLE_0:def_3; hence z = [(z `1),(z `2)] by H2; ::_thesis: verum end; definition let L be non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr ; let z be rational_function of L; attrz is irreducible means :defirred: :: RATFUNC1:def 10 z `1 ,z `2 have_no_common_roots ; end; :: deftheorem defirred defines irreducible RATFUNC1:def_10_:_ for L being non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr for z being rational_function of L holds ( z is irreducible iff z `1 ,z `2 have_no_common_roots ); notation let L be non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr ; let z be rational_function of L; antonym reducible z for irreducible ; end; definition let L be non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr ; let z be rational_function of L; attrz is normalized means :defnorm: :: RATFUNC1:def 11 ( z is irreducible & z `2 is normalized ); end; :: deftheorem defnorm defines normalized RATFUNC1:def_11_:_ for L being non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr for z being rational_function of L holds ( z is normalized iff ( z is irreducible & z `2 is normalized ) ); registration let L be non trivial right_complementable unital distributive add-associative right_zeroed doubleLoopStr ; cluster normalized -> irreducible for rational_function of L; coherence for b1 being rational_function of L st b1 is normalized holds b1 is irreducible by defnorm; end; registration let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be rational_function of L; cluster Leading-Coefficient (z `2) -> non zero ; coherence not LC (z `2) is zero ; end; definition let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be rational_function of L; func NormRationalFunction z -> rational_function of L equals :: RATFUNC1:def 12 [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))]; coherence [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))] is rational_function of L ; end; :: deftheorem defines NormRationalFunction RATFUNC1:def_12_:_ for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being rational_function of L holds NormRationalFunction z = [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))]; notation let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be rational_function of L; synonym NormRatF z for NormRationalFunction z; end; registration let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be non zero rational_function of L; cluster NormRationalFunction z -> non zero ; coherence not NormRationalFunction z is zero proof z `1 <> 0_. L by defzerrat; then reconsider z1 = z `1 as non zero Polynomial of L by defzer; not ((1. L) / (LC (z `2))) * z1 is zero ; then (NormRatF z) `1 <> 0_. L by XTUPLE_0:def_2; hence not NormRationalFunction z is zero by defzerrat; ::_thesis: verum end; end; definition let L be non degenerated multLoopStr_0 ; func 0._ L -> rational_function of L equals :: RATFUNC1:def 13 [(0_. L),(1_. L)]; coherence [(0_. L),(1_. L)] is rational_function of L ; func 1._ L -> rational_function of L equals :: RATFUNC1:def 14 [(1_. L),(1_. L)]; coherence [(1_. L),(1_. L)] is rational_function of L ; end; :: deftheorem defines 0._ RATFUNC1:def_13_:_ for L being non degenerated multLoopStr_0 holds 0._ L = [(0_. L),(1_. L)]; :: deftheorem defines 1._ RATFUNC1:def_14_:_ for L being non degenerated multLoopStr_0 holds 1._ L = [(1_. L),(1_. L)]; registration let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ; cluster 0._ L -> normalized ; coherence 0._ L is normalized proof set z = [(0_. L),(1_. L)]; set p1 = [(0_. L),(1_. L)] `1 ; set p2 = [(0_. L),(1_. L)] `2 ; now__::_thesis:_not_[(0_._L),(1_._L)]_`1_,[(0_._L),(1_._L)]_`2_have_a_common_root assume [(0_. L),(1_. L)] `1 ,[(0_. L),(1_. L)] `2 have_a_common_root ; ::_thesis: contradiction then consider x being Element of L such that B: x is_a_common_root_of [(0_. L),(1_. L)] `1 ,[(0_. L),(1_. L)] `2 by root2; x is_a_root_of [(0_. L),(1_. L)] `2 by B, root1; then eval (([(0_. L),(1_. L)] `2),x) = 0. L by POLYNOM5:def_6; hence contradiction by POLYNOM4:18; ::_thesis: verum end; then B: [(0_. L),(1_. L)] is irreducible by defirred; C: len (1_. L) = 1 by POLYNOM4:4; (len (1_. L)) -' 1 = 1 - 1 by C, XREAL_0:def_2; then LC (1_. L) = 1. L by POLYNOM3:30; then [(0_. L),(1_. L)] `2 is normalized by defnormp; hence 0._ L is normalized by B, defnorm; ::_thesis: verum end; end; registration let L be non degenerated multLoopStr_0 ; cluster 1._ L -> non zero ; coherence not 1._ L is zero proof (1._ L) `1 <> 0_. L by XTUPLE_0:def_2; hence not 1._ L is zero by defzerrat; ::_thesis: verum end; end; registration let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ; cluster 1._ L -> irreducible ; coherence 1._ L is irreducible proof set z = [(1_. L),(1_. L)]; set p1 = [(1_. L),(1_. L)] `1 ; set p2 = [(1_. L),(1_. L)] `2 ; now__::_thesis:_not_[(1_._L),(1_._L)]_`1_,[(1_._L),(1_._L)]_`2_have_a_common_root assume [(1_. L),(1_. L)] `1 ,[(1_. L),(1_. L)] `2 have_a_common_root ; ::_thesis: contradiction then consider x being Element of L such that B: x is_a_common_root_of [(1_. L),(1_. L)] `1 ,[(1_. L),(1_. L)] `2 by root2; x is_a_root_of [(1_. L),(1_. L)] `2 by B, root1; then eval (([(1_. L),(1_. L)] `2),x) = 0. L by POLYNOM5:def_6; hence contradiction by POLYNOM4:18; ::_thesis: verum end; hence 1._ L is irreducible by defirred; ::_thesis: verum end; end; registration let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ; cluster non zero irreducible for rational_function of L; existence ex b1 being rational_function of L st ( b1 is irreducible & not b1 is zero ) proof take 1._ L ; ::_thesis: ( 1._ L is irreducible & not 1._ L is zero ) thus ( 1._ L is irreducible & not 1._ L is zero ) ; ::_thesis: verum end; end; registration let L be non degenerated right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; let x be Element of L; cluster[(rpoly (1,x)),(rpoly (1,x))] -> non zero reducible for rational_function of L; coherence for b1 being rational_function of L st b1 = [(rpoly (1,x)),(rpoly (1,x))] holds ( not b1 is irreducible & not b1 is zero ) proof set z = [(rpoly (1,x)),(rpoly (1,x))]; C: [(rpoly (1,x)),(rpoly (1,x))] `1 = rpoly (1,x) ; x is_a_root_of rpoly (1,x) by HURWITZ:30; then x is_a_root_of [(rpoly (1,x)),(rpoly (1,x))] `1 ; then x is_a_common_root_of [(rpoly (1,x)),(rpoly (1,x))] `1 ,[(rpoly (1,x)),(rpoly (1,x))] `2 by root1; then [(rpoly (1,x)),(rpoly (1,x))] `1 ,[(rpoly (1,x)),(rpoly (1,x))] `2 have_common_roots by root2; then [(rpoly (1,x)),(rpoly (1,x))] is reducible by defirred; hence for b1 being rational_function of L st b1 = [(rpoly (1,x)),(rpoly (1,x))] holds ( not b1 is irreducible & not b1 is zero ) by C, defzerrat; ::_thesis: verum end; end; registration let L be non degenerated right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; cluster non zero reducible for rational_function of L; existence ex b1 being rational_function of L st ( b1 is reducible & not b1 is zero ) proof set x = the Element of L; take z = [(rpoly (1, the Element of L)),(rpoly (1, the Element of L))]; ::_thesis: ( z is reducible & not z is zero ) thus ( z is reducible & not z is zero ) ; ::_thesis: verum end; end; registration let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ; cluster normalized for rational_function of L; existence ex b1 being rational_function of L st b1 is normalized proof take 0._ L ; ::_thesis: 0._ L is normalized thus 0._ L is normalized ; ::_thesis: verum end; end; registration let L be non degenerated multLoopStr_0 ; cluster 0._ L -> zero ; coherence 0._ L is zero proof (0._ L) `1 = 0_. L by XTUPLE_0:def_2; hence 0._ L is zero by defzerrat; ::_thesis: verum end; end; registration let L be non degenerated right_complementable associative well-unital distributive add-associative right_zeroed doubleLoopStr ; cluster 1._ L -> normalized ; coherence 1._ L is normalized proof len (1_. L) = 1 by POLYNOM4:4; then (len (1_. L)) -' 1 = 1 - 1 by XREAL_0:def_2; then LC (1_. L) = 1. L by POLYNOM3:30; then [(1_. L),(1_. L)] `2 is normalized by defnormp; hence 1._ L is normalized by defnorm; ::_thesis: verum end; end; definition let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; let p, q be rational_function of L; funcp + q -> rational_function of L equals :: RATFUNC1:def 15 [(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))]; coherence [(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))] is rational_function of L ; end; :: deftheorem defines + RATFUNC1:def_15_:_ for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being rational_function of L holds p + q = [(((p `1) *' (q `2)) + ((p `2) *' (q `1))),((p `2) *' (q `2))]; definition let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; let p, q be rational_function of L; funcp *' q -> rational_function of L equals :: RATFUNC1:def 16 [((p `1) *' (q `1)),((p `2) *' (q `2))]; coherence [((p `1) *' (q `1)),((p `2) *' (q `2))] is rational_function of L ; end; :: deftheorem defines *' RATFUNC1:def_16_:_ for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being rational_function of L holds p *' q = [((p `1) *' (q `1)),((p `2) *' (q `2))]; theorem tw2: :: RATFUNC1:20 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for p being rational_function of L for a being non zero Element of L holds ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible ) proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being rational_function of L for a being non zero Element of L holds ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible ) let p be rational_function of L; ::_thesis: for a being non zero Element of L holds ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible ) let a be non zero Element of L; ::_thesis: ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible ) set ap = [(a * (p `1)),(a * (p `2))]; A: now__::_thesis:_(_p_is_irreducible_&_[(a_*_(p_`1)),(a_*_(p_`2))]_is_reducible_implies_[(a_*_(p_`1)),(a_*_(p_`2))]_is_irreducible_) assume A0: p is irreducible ; ::_thesis: ( [(a * (p `1)),(a * (p `2))] is reducible implies [(a * (p `1)),(a * (p `2))] is irreducible ) assume [(a * (p `1)),(a * (p `2))] is reducible ; ::_thesis: [(a * (p `1)),(a * (p `2))] is irreducible then [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 have_common_roots by defirred; then consider x being Element of L such that A1: x is_a_common_root_of [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 by root2; ( x is_a_root_of [(a * (p `1)),(a * (p `2))] `1 & x is_a_root_of [(a * (p `1)),(a * (p `2))] `2 ) by A1, root1; then A2: ( eval (([(a * (p `1)),(a * (p `2))] `1),x) = 0. L & eval (([(a * (p `1)),(a * (p `2))] `2),x) = 0. L ) by POLYNOM5:def_6; then eval ((a * (p `1)),x) = 0. L ; then a * (eval ((p `1),x)) = 0. L by POLYNOM5:30; then eval ((p `1),x) = 0. L by VECTSP_2:def_1; then A3: x is_a_root_of p `1 by POLYNOM5:def_6; eval ((a * (p `2)),x) = 0. L by A2; then a * (eval ((p `2),x)) = 0. L by POLYNOM5:30; then eval ((p `2),x) = 0. L by VECTSP_2:def_1; then x is_a_root_of p `2 by POLYNOM5:def_6; then x is_a_common_root_of p `1 ,p `2 by A3, root1; then p `1 ,p `2 have_common_roots by root2; hence [(a * (p `1)),(a * (p `2))] is irreducible by A0, defirred; ::_thesis: verum end; now__::_thesis:_(_[(a_*_(p_`1)),(a_*_(p_`2))]_is_irreducible_&_p_is_reducible_implies_p_is_irreducible_) assume A0: [(a * (p `1)),(a * (p `2))] is irreducible ; ::_thesis: ( p is reducible implies p is irreducible ) assume p is reducible ; ::_thesis: p is irreducible then p `1 ,p `2 have_common_roots by defirred; then consider x being Element of L such that A1: x is_a_common_root_of p `1 ,p `2 by root2; ( x is_a_root_of p `1 & x is_a_root_of p `2 ) by A1, root1; then A2: ( eval ((p `1),x) = 0. L & eval ((p `2),x) = 0. L ) by POLYNOM5:def_6; then a * (eval ((p `1),x)) = 0. L by VECTSP_1:6; then eval ((a * (p `1)),x) = 0. L by POLYNOM5:30; then eval (([(a * (p `1)),(a * (p `2))] `1),x) = 0. L ; then A3: x is_a_root_of [(a * (p `1)),(a * (p `2))] `1 by POLYNOM5:def_6; a * (eval ((p `2),x)) = 0. L by A2, VECTSP_1:6; then eval ((a * (p `2)),x) = 0. L by POLYNOM5:30; then eval (([(a * (p `1)),(a * (p `2))] `2),x) = 0. L ; then x is_a_root_of [(a * (p `1)),(a * (p `2))] `2 by POLYNOM5:def_6; then x is_a_common_root_of [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 by A3, root1; then [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 have_common_roots by root2; hence p is irreducible by A0, defirred; ::_thesis: verum end; hence ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible ) by A; ::_thesis: verum end; begin polynormirred: for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being rational_function of L st z is irreducible holds ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) proof let L be non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L st z is irreducible holds ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) let z be rational_function of L; ::_thesis: ( z is irreducible implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) assume AS: z is irreducible ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) take z ; ::_thesis: ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z `1)),(z2 *' (z `2))] & z is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) reconsider e = 1_. L as non zero Polynomial of L ; take e ; ::_thesis: ( z = [(e *' (z `1)),(e *' (z `2))] & z is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( e = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) reconsider f = <*> the carrier of (Polynom-Ring L) as FinSequence of (Polynom-Ring L) ; thus z = [(z `1),(z `2)] by ttt .= [(e *' (z `1)),(z `2)] by POLYNOM3:35 .= [(e *' (z `1)),(e *' (z `2))] by POLYNOM3:35 ; ::_thesis: ( z is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( e = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) thus z is irreducible by AS; ::_thesis: ex f being FinSequence of (Polynom-Ring L) st ( e = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) take f ; ::_thesis: ( e = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) Product f = 1_ (Polynom-Ring L) by GROUP_4:8; hence ( e = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by POLYNOM3:def_10; ::_thesis: verum end; theorem ratfuncNF: :: RATFUNC1:21 for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being rational_function of L ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) proof let L be non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) let z be rational_function of L; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) defpred S1[ Nat] means for z being rational_function of L st max ((deg (z `1)),(deg (z `2))) = $1 holds ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ); now__::_thesis:_for_z_being_rational_function_of_L_st_max_((deg_(z_`1)),(deg_(z_`2)))_=_0_holds_ ex_z1_being_rational_function_of_L_ex_z2_being_non_zero_Polynomial_of_L_st_ (_z_=_[(z2_*'_(z1_`1)),(z2_*'_(z1_`2))]_&_z1_is_irreducible_&_ex_f_being_FinSequence_of_(Polynom-Ring_L)_st_ (_z2_=_Product_f_&_(_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_ ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_z_`1_,z_`2_&_f_._i_=_rpoly_(1,x)_)_)_)_) let z be rational_function of L; ::_thesis: ( max ((deg (z `1)),(deg (z `2))) = 0 implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) assume max ((deg (z `1)),(deg (z `2))) = 0 ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) then deg (z `2) <= 0 by XXREAL_0:25; then B: deg (z `2) = 0 ; A: now__::_thesis:_for_x_being_Element_of_L_holds_not_x_is_a_root_of_z_`2 assume ex x being Element of L st x is_a_root_of z `2 ; ::_thesis: contradiction then consider y being Element of L such that H: y is_a_root_of z `2 ; eval ((z `2),y) = 0. L by H, POLYNOM5:def_6; hence contradiction by B, degrat2; ::_thesis: verum end; now__::_thesis:_not_z_is_reducible assume z is reducible ; ::_thesis: contradiction then z `1 ,z `2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z `1 ,z `2 by root2; x is_a_root_of z `2 by H, root1; hence contradiction by A; ::_thesis: verum end; hence ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by polynormirred; ::_thesis: verum end; then IA: S1[ 0 ] ; IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume AS: S1[n] ; ::_thesis: S1[n + 1] for z being rational_function of L st max ((deg (z `1)),(deg (z `2))) = n + 1 holds ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) proof let z be rational_function of L; ::_thesis: ( max ((deg (z `1)),(deg (z `2))) = n + 1 implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) assume AS1: max ((deg (z `1)),(deg (z `2))) = n + 1 ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) percases ( z is irreducible or z is reducible ) ; suppose z is irreducible ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) hence ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by polynormirred; ::_thesis: verum end; suppose z is reducible ; ::_thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) then z `1 ,z `2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z `1 ,z `2 by root2; H3: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by H, root1; consider q2 being Polynomial of L such that H2: z `2 = (rpoly (1,x)) *' q2 by H3, HURWITZ:33; consider q1 being Polynomial of L such that H1: z `1 = (rpoly (1,x)) *' q1 by H3, HURWITZ:33; q2 <> 0_. L by H2, POLYNOM3:34; then reconsider q2 = q2 as non zero Polynomial of L by defzer; set q = [q1,q2]; max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n proof A2: deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by H2, HURWITZ:23 .= 1 + (deg q2) by HURWITZ:27 ; percases ( max ((deg (z `1)),(deg (z `2))) = deg (z `1) or max ((deg (z `1)),(deg (z `2))) = deg (z `2) ) by XXREAL_0:16; supposeA5: max ((deg (z `1)),(deg (z `2))) = deg (z `1) ; ::_thesis: max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n then z `1 <> 0_. L by AS1, HURWITZ:20; then q1 <> 0_. L by H1, POLYNOM3:34; then A3: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by H1, HURWITZ:23 .= 1 + (deg q1) by HURWITZ:27 ; A6: deg (z `2) <= n + 1 by AS1, XXREAL_0:25; ((deg q2) + 1) - 1 <= (n + 1) - 1 by A2, A6, XREAL_1:9; hence max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n by A3, A5, AS1, XXREAL_0:def_10; ::_thesis: verum end; supposeA3: max ((deg (z `1)),(deg (z `2))) = deg (z `2) ; ::_thesis: max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n A6: deg (z `1) <= n + 1 by AS1, XXREAL_0:25; now__::_thesis:_deg_q1_<=_deg_q2 percases ( q1 = 0_. L or q1 <> 0_. L ) ; suppose q1 = 0_. L ; ::_thesis: deg q1 <= deg q2 hence deg q1 <= deg q2 by HURWITZ:20; ::_thesis: verum end; suppose q1 <> 0_. L ; ::_thesis: deg q1 <= deg q2 then deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by H1, HURWITZ:23 .= 1 + (deg q1) by HURWITZ:27 ; hence deg q1 <= deg q2 by A6, A2, A3, AS1, XREAL_1:9; ::_thesis: verum end; end; end; hence max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n by A3, A2, AS1, XXREAL_0:def_10; ::_thesis: verum end; end; end; then consider z1q being rational_function of L, z2q being non zero Polynomial of L such that IQ: ( [q1,q2] = [(z2q *' (z1q `1)),(z2q *' (z1q `2))] & z1q is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2q = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & f . i = rpoly (1,x) ) ) ) ) by AS; take z1 = z1q; ::_thesis: ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) set z2 = (rpoly (1,x)) *' z2q; reconsider z2 = (rpoly (1,x)) *' z2q as non zero Polynomial of L ; take z2 ; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) consider fq being FinSequence of (Polynom-Ring L) such that IQ2: ( z2q = Product fq & ( for i being Element of NAT st i in dom fq holds ex x being Element of L st ( x is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & fq . i = rpoly (1,x) ) ) ) by IQ; reconsider rp = rpoly (1,x) as Element of (Polynom-Ring L) by POLYNOM3:def_10; set f = <*rp*> ^ fq; IQ3: Product (<*rp*> ^ fq) = rp * (Product fq) by GROUP_4:7 .= z2 by IQ2, POLYNOM3:def_10 ; IQ4: z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] proof X: q1 = z2q *' (z1q `1) by IQ, XTUPLE_0:def_2; Z: q2 = z2q *' (z1q `2) by IQ, XTUPLE_0:def_3; Y: z2 *' (z1 `1) = z `1 by X, H1, POLYNOM3:33; A: z2 *' (z1 `2) = z `2 by Z, H2, POLYNOM3:33; thus z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] by Y, A, ttt; ::_thesis: verum end; IQ5: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(<*rp*>_^_fq)_holds_ ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_z_`1_,z_`2_&_(<*rp*>_^_fq)_._i_=_rpoly_(1,x)_) let i be Element of NAT ; ::_thesis: ( i in dom (<*rp*> ^ fq) implies ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) ) assume C1: i in dom (<*rp*> ^ fq) ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) now__::_thesis:_ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_z_`1_,z_`2_&_(<*rp*>_^_fq)_._i_=_rpoly_(1,x)_) percases ( i in dom <*rp*> or ex n being Nat st ( n in dom fq & i = (len <*rp*>) + n ) ) by C1, FINSEQ_1:25; supposeC2: i in dom <*rp*> ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) then C3: i in {1} by FINSEQ_1:2, FINSEQ_1:38; (<*rp*> ^ fq) . i = <*rp*> . i by C2, FINSEQ_1:def_7 .= <*rp*> . 1 by C3, TARSKI:def_1 .= rpoly (1,x) by FINSEQ_1:40 ; hence ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) by H; ::_thesis: verum end; suppose ex n being Nat st ( n in dom fq & i = (len <*rp*>) + n ) ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) then consider n being Nat such that C2: ( n in dom fq & i = (len <*rp*>) + n ) ; (<*rp*> ^ fq) . i = fq . n by C2, FINSEQ_1:def_7; then consider y being Element of L such that C3: ( y is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & (<*rp*> ^ fq) . i = rpoly (1,y) ) by C2, IQ2; C4: ( y is_a_root_of [q1,q2] `1 & y is_a_root_of [q1,q2] `2 ) by C3, root1; then C5: 0. L = eval (q1,y) by POLYNOM5:def_6; C8: eval ((z `1),y) = (eval ((rpoly (1,x)),y)) * (eval (q1,y)) by H1, POLYNOM4:24 .= 0. L by C5, VECTSP_1:7 ; C6: 0. L = eval (q2,y) by C4, POLYNOM5:def_6; eval ((z `2),y) = (eval ((rpoly (1,x)),y)) * (eval (q2,y)) by H2, POLYNOM4:24 .= 0. L by C6, VECTSP_1:7 ; then ( y is_a_root_of z `1 & y is_a_root_of z `2 ) by C8, POLYNOM5:def_6; then y is_a_common_root_of z `1 ,z `2 by root1; hence ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) by C3; ::_thesis: verum end; end; end; hence ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) ; ::_thesis: verum end; thus ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by IQ, IQ3, IQ4, IQ5; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS); max ((deg (z `1)),(deg (z `2))) >= deg (z `2) by XXREAL_0:25; then max ((deg (z `1)),(deg (z `2))) >= 0 ; then max ((deg (z `1)),(deg (z `2))) in NAT by INT_1:3; hence ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by I; ::_thesis: verum end; ratfuncNFunique1: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being rational_function of L st z is irreducible holds for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L st z is irreducible holds for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) let z be rational_function of L; ::_thesis: ( z is irreducible implies for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) ) assume AS: z is irreducible ; ::_thesis: for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) let z2 be non zero Polynomial of L; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) ) assume A: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) let g1 be rational_function of L; ::_thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) let g2 be non zero Polynomial of L; ::_thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) ) assume B: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( g2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) consider f being FinSequence of (Polynom-Ring L) such that C: ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by A; now__::_thesis:_(_f_<>_<*>_the_carrier_of_(Polynom-Ring_L)_implies_for_i_being_Element_of_dom_f_holds_contradiction_) assume f <> <*> the carrier of (Polynom-Ring L) ; ::_thesis: for i being Element of dom f holds contradiction then G: dom f <> {} ; let i be Element of dom f; ::_thesis: contradiction reconsider i = i as Nat ; D1: i in dom f by G; consider x being Element of L such that D2: ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by D1, C; z `1 ,z `2 have_common_roots by D2, root2; hence contradiction by AS, defirred; ::_thesis: verum end; hence D2: z2 = 1_ (Polynom-Ring L) by C, GROUP_4:8 .= 1_. L by POLYNOM3:def_10 ; ::_thesis: ( g2 = 1_. L & z1 = g1 ) then D1: z2 *' (z1 `1) = z1 `1 by POLYNOM3:35; z2 *' (z1 `2) = z1 `2 by D2, POLYNOM3:35; then D: z = z1 by D1, A, ttt; consider h being FinSequence of (Polynom-Ring L) such that E: ( g2 = Product h & ( for i being Element of NAT st i in dom h holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & h . i = rpoly (1,x) ) ) ) by B; now__::_thesis:_(_h_<>_<*>_the_carrier_of_(Polynom-Ring_L)_implies_for_i_being_Element_of_dom_h_holds_contradiction_) assume h <> <*> the carrier of (Polynom-Ring L) ; ::_thesis: for i being Element of dom h holds contradiction then G: dom h <> {} ; let i be Element of dom h; ::_thesis: contradiction reconsider i = i as Nat ; D1: i in dom h by G; consider x being Element of L such that D2: ( x is_a_common_root_of z `1 ,z `2 & h . i = rpoly (1,x) ) by D1, E; z `1 ,z `2 have_common_roots by D2, root2; hence contradiction by AS, defirred; ::_thesis: verum end; hence E2: g2 = 1_ (Polynom-Ring L) by E, GROUP_4:8 .= 1_. L by POLYNOM3:def_10 ; ::_thesis: z1 = g1 then E1: g2 *' (g1 `1) = g1 `1 by POLYNOM3:35; g2 *' (g1 `2) = g1 `2 by E2, POLYNOM3:35; hence z1 = g1 by D, E1, B, ttt; ::_thesis: verum end; ratfuncNFunique2: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being non zero rational_function of L for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 proof let L be Field; ::_thesis: for z being non zero rational_function of L for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 let z be non zero rational_function of L; ::_thesis: for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 let z2 be non zero Polynomial of L; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 ) assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 let g1 be rational_function of L; ::_thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 let g2 be non zero Polynomial of L; ::_thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) implies z1 = g1 ) assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; ::_thesis: z1 = g1 defpred S1[ Nat] means for z being non zero rational_function of L st max ((deg (z `1)),(deg (z `2))) = $1 holds for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1; now__::_thesis:_for_z_being_non_zero_rational_function_of_L_st_max_((deg_(z_`1)),(deg_(z_`2)))_=_0_holds_ for_z1_being_rational_function_of_L for_z2_being_non_zero_Polynomial_of_L_st_z_=_[(z2_*'_(z1_`1)),(z2_*'_(z1_`2))]_&_z1_is_irreducible_&_ex_f_being_FinSequence_of_(Polynom-Ring_L)_st_ (_z2_=_Product_f_&_(_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_ ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_z_`1_,z_`2_&_f_._i_=_rpoly_(1,x)_)_)_)_holds_ for_g1_being_rational_function_of_L for_g2_being_non_zero_Polynomial_of_L_st_z_=_[(g2_*'_(g1_`1)),(g2_*'_(g1_`2))]_&_g1_is_irreducible_&_ex_g_being_FinSequence_of_(Polynom-Ring_L)_st_ (_g2_=_Product_g_&_(_for_i_being_Element_of_NAT_st_i_in_dom_g_holds_ ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_z_`1_,z_`2_&_g_._i_=_rpoly_(1,x)_)_)_)_holds_ g1_=_z1 let z be non zero rational_function of L; ::_thesis: ( max ((deg (z `1)),(deg (z `2))) = 0 implies for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds g1 = z1 ) assume max ((deg (z `1)),(deg (z `2))) = 0 ; ::_thesis: for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds g1 = z1 then deg (z `2) <= 0 by XXREAL_0:25; then B: deg (z `2) = 0 ; let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds g1 = z1 let z2 be non zero Polynomial of L; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds g1 = z1 ) assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds g1 = z1 let g1 be rational_function of L; ::_thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds g1 = z1 let g2 be non zero Polynomial of L; ::_thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) implies g1 = z1 ) assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; ::_thesis: g1 = z1 A: now__::_thesis:_for_x_being_Element_of_L_holds_not_x_is_a_root_of_z_`2 assume ex x being Element of L st x is_a_root_of z `2 ; ::_thesis: contradiction then consider y being Element of L such that H: y is_a_root_of z `2 ; eval ((z `2),y) = 0. L by H, POLYNOM5:def_6; hence contradiction by B, degrat2; ::_thesis: verum end; B: now__::_thesis:_not_z_is_reducible assume z is reducible ; ::_thesis: contradiction then z `1 ,z `2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z `1 ,z `2 by root2; x is_a_root_of z `2 by H, root1; hence contradiction by A; ::_thesis: verum end; thus g1 = z1 by B, H1, H2, ratfuncNFunique1; ::_thesis: verum end; then IA: S1[ 0 ] ; IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume IV: S1[n] ; ::_thesis: S1[n + 1] for z being non zero rational_function of L st max ((deg (z `1)),(deg (z `2))) = n + 1 holds for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 proof let z be non zero rational_function of L; ::_thesis: ( max ((deg (z `1)),(deg (z `2))) = n + 1 implies for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 ) assume AS1: max ((deg (z `1)),(deg (z `2))) = n + 1 ; ::_thesis: for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 let z2 be non zero Polynomial of L; ::_thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 ) assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; ::_thesis: for g1 being rational_function of L for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 consider f being FinSequence of (Polynom-Ring L) such that H1a: ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by H1; let g1 be rational_function of L; ::_thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds z1 = g1 let g2 be non zero Polynomial of L; ::_thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) implies z1 = g1 ) assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; ::_thesis: z1 = g1 consider g being FinSequence of (Polynom-Ring L) such that H2a: ( g2 = Product g & ( for i being Element of NAT st i in dom g holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) by H2; percases ( z is irreducible or z is reducible ) ; supposeB: z is irreducible ; ::_thesis: z1 = g1 thus g1 = z1 by B, H1, H2, ratfuncNFunique1; ::_thesis: verum end; suppose z is reducible ; ::_thesis: z1 = g1 then z `1 ,z `2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z `1 ,z `2 by root2; H3: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by H, root1; consider q2 being Polynomial of L such that HY: z `2 = (rpoly (1,x)) *' q2 by H3, HURWITZ:33; consider q1 being Polynomial of L such that HX: z `1 = (rpoly (1,x)) *' q1 by H3, HURWITZ:33; q2 <> 0_. L by HY, POLYNOM3:34; then reconsider q2 = q2 as non zero Polynomial of L by defzer; set q = [q1,q2]; z `1 <> 0_. L by defzerrat; then q1 <> 0_. L by HX, POLYNOM3:34; then [q1,q2] `1 <> 0_. L ; then reconsider q = [q1,q2] as non zero rational_function of L by defzerrat; AS2: max ((deg (q `1)),(deg (q `2))) = n proof A2: deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by HY, HURWITZ:23 .= 1 + (deg q2) by HURWITZ:27 ; A7: max ((deg (q `1)),(deg (q `2))) = max ((deg q1),(deg (q `2))) by XTUPLE_0:def_2 .= max ((deg q1),(deg q2)) by XTUPLE_0:def_3 ; percases ( max ((deg (z `1)),(deg (z `2))) = deg (z `1) or max ((deg (z `1)),(deg (z `2))) = deg (z `2) ) by XXREAL_0:16; supposeA5: max ((deg (z `1)),(deg (z `2))) = deg (z `1) ; ::_thesis: max ((deg (q `1)),(deg (q `2))) = n then z `1 <> 0_. L by AS1, HURWITZ:20; then q1 <> 0_. L by HX, POLYNOM3:34; then A3: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23 .= 1 + (deg q1) by HURWITZ:27 ; deg (z `2) <= n + 1 by AS1, XXREAL_0:25; then ((deg q2) + 1) - 1 <= (n + 1) - 1 by A2, XREAL_1:9; hence max ((deg (q `1)),(deg (q `2))) = n by A7, A3, A5, AS1, XXREAL_0:def_10; ::_thesis: verum end; supposeA3: max ((deg (z `1)),(deg (z `2))) = deg (z `2) ; ::_thesis: max ((deg (q `1)),(deg (q `2))) = n A6: deg (z `1) <= n + 1 by AS1, XXREAL_0:25; now__::_thesis:_deg_q1_<=_deg_q2 percases ( q1 = 0_. L or q1 <> 0_. L ) ; suppose q1 = 0_. L ; ::_thesis: deg q1 <= deg q2 hence deg q1 <= deg q2 by HURWITZ:20; ::_thesis: verum end; suppose q1 <> 0_. L ; ::_thesis: deg q1 <= deg q2 then deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23 .= 1 + (deg q1) by HURWITZ:27 ; hence deg q1 <= deg q2 by A6, A3, A2, AS1, XREAL_1:9; ::_thesis: verum end; end; end; hence max ((deg (q `1)),(deg (q `2))) = n by A7, A2, A3, AS1, XXREAL_0:def_10; ::_thesis: verum end; end; end; ZZ1: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f_holds_ ex_z_being_Element_of_L_st_f_._i_=_rpoly_(1,z) let i be Nat; ::_thesis: ( i in dom f implies ex z being Element of L st f . i = rpoly (1,z) ) assume i in dom f ; ::_thesis: ex z being Element of L st f . i = rpoly (1,z) then ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by H1a; hence ex z being Element of L st f . i = rpoly (1,z) ; ::_thesis: verum end; ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) proof z2 *' (z1 `1) = (rpoly (1,x)) *' q1 by HX, H1, XTUPLE_0:def_2; then Z11: rpoly (1,x) divides z2 *' (z1 `1) by HURWITZ:34; z2 *' (z1 `2) = (rpoly (1,x)) *' q2 by HY, H1, XTUPLE_0:def_3; then Z11a: rpoly (1,x) divides z2 *' (z1 `2) by HURWITZ:34; now__::_thesis:_(_(_rpoly_(1,x)_divides_z2_&_ex_i,_i_being_Nat_st_ (_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)_)_or_(_rpoly_(1,x)_divides_z1_`1_&_rpoly_(1,x)_divides_z1_`2_&_ex_i_being_Nat_st_ (_i_in_dom_f_&_f_._i_=_rpoly_(1,x)_)_)_) percases ( rpoly (1,x) divides z2 or ( rpoly (1,x) divides z1 `1 & rpoly (1,x) divides z1 `2 ) ) by Z11, Z11a, div3; case rpoly (1,x) divides z2 ; ::_thesis: ex i, i being Nat st ( i in dom f & f . i = rpoly (1,x) ) then eval (z2,x) = 0. L by div1; then consider i being Nat such that Z3: ( i in dom f & f . i = rpoly (1,x) ) by div2, H1a, ZZ1; take i = i; ::_thesis: ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) thus ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) by Z3; ::_thesis: verum end; case ( rpoly (1,x) divides z1 `1 & rpoly (1,x) divides z1 `2 ) ; ::_thesis: ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) then ( eval ((z1 `1),x) = 0. L & eval ((z1 `2),x) = 0. L ) by div1; then ( x is_a_root_of z1 `1 & x is_a_root_of z1 `2 ) by POLYNOM5:def_6; then Z3: x is_a_common_root_of z1 `1 ,z1 `2 by root1; z1 `1 ,z1 `2 have_no_common_roots by H1, defirred; hence ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) by Z3, root2; ::_thesis: verum end; end; end; hence ex i being Nat st ( i in dom f & f . i = rpoly (1,x) ) ; ::_thesis: verum end; then consider i being Nat such that H5: ( i in dom f & f . i = rpoly (1,x) ) ; ZZ1a: now__::_thesis:_for_j_being_Nat_st_j_in_dom_g_holds_ ex_z_being_Element_of_L_st_g_._j_=_rpoly_(1,z) let j be Nat; ::_thesis: ( j in dom g implies ex z being Element of L st g . j = rpoly (1,z) ) assume j in dom g ; ::_thesis: ex z being Element of L st g . j = rpoly (1,z) then consider x being Element of L such that A: ( x is_a_common_root_of z `1 ,z `2 & g . j = rpoly (1,x) ) by H2a; thus ex z being Element of L st g . j = rpoly (1,z) by A; ::_thesis: verum end; ex j being Nat st ( j in dom g & g . j = rpoly (1,x) ) proof g2 *' (g1 `1) = (rpoly (1,x)) *' q1 by HX, H2, XTUPLE_0:def_2; then Z11: rpoly (1,x) divides g2 *' (g1 `1) by HURWITZ:34; g2 *' (g1 `2) = (rpoly (1,x)) *' q2 by HY, H2, XTUPLE_0:def_3; then Z11a: rpoly (1,x) divides g2 *' (g1 `2) by HURWITZ:34; now__::_thesis:_(_(_rpoly_(1,x)_divides_g2_&_ex_i,_j_being_Nat_st_ (_j_in_dom_g_&_g_._j_=_rpoly_(1,x)_)_)_or_(_rpoly_(1,x)_divides_g1_`1_&_rpoly_(1,x)_divides_g1_`2_&_ex_j_being_Nat_st_ (_j_in_dom_g_&_g_._j_=_rpoly_(1,x)_)_)_) percases ( rpoly (1,x) divides g2 or ( rpoly (1,x) divides g1 `1 & rpoly (1,x) divides g1 `2 ) ) by Z11, Z11a, div3; case rpoly (1,x) divides g2 ; ::_thesis: ex i, j being Nat st ( j in dom g & g . j = rpoly (1,x) ) then eval (g2,x) = 0. L by div1; then consider i being Nat such that Z3: ( i in dom g & g . i = rpoly (1,x) ) by div2, H2a, ZZ1a; take i = i; ::_thesis: ex j being Nat st ( j in dom g & g . j = rpoly (1,x) ) thus ex j being Nat st ( j in dom g & g . j = rpoly (1,x) ) by Z3; ::_thesis: verum end; case ( rpoly (1,x) divides g1 `1 & rpoly (1,x) divides g1 `2 ) ; ::_thesis: ex j being Nat st ( j in dom g & g . j = rpoly (1,x) ) then ( eval ((g1 `1),x) = 0. L & eval ((g1 `2),x) = 0. L ) by div1; then ( x is_a_root_of g1 `1 & x is_a_root_of g1 `2 ) by POLYNOM5:def_6; then Z3: x is_a_common_root_of g1 `1 ,g1 `2 by root1; g1 `1 ,g1 `2 have_no_common_roots by H2, defirred; hence ex j being Nat st ( j in dom g & g . j = rpoly (1,x) ) by Z3, root2; ::_thesis: verum end; end; end; hence ex j being Nat st ( j in dom g & g . j = rpoly (1,x) ) ; ::_thesis: verum end; then consider j being Nat such that H6: ( j in dom g & g . j = rpoly (1,x) ) ; reconsider fq = Del (f,i) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105; reconsider gq = Del (g,j) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105; X100: now__::_thesis:_for_k_being_Nat_st_k_in_dom_fq_holds_ ex_x_being_Element_of_L_st_fq_._k_=_rpoly_(1,x) let k be Nat; ::_thesis: ( k in dom fq implies ex x being Element of L st fq . k = rpoly (1,x) ) assume H11: k in dom fq ; ::_thesis: ex x being Element of L st fq . k = rpoly (1,x) consider m being Nat such that H14: ( len f = m + 1 & len fq = m ) by H5, FINSEQ_3:104; H14a: k in Seg m by H11, H14, FINSEQ_1:def_3; Seg m c= Seg (m + 1) by FINSEQ_3:18; then k in Seg (m + 1) by H14a; then H13: k in dom f by H14, FINSEQ_1:def_3; H14b: k <= m by H14a, FINSEQ_1:1; then H14d: k + 1 <= m + 1 by XREAL_1:6; 1 <= k + 1 by NAT_1:11; then k + 1 in Seg (m + 1) by H14d; then H14c: k + 1 in dom f by H14, FINSEQ_1:def_3; now__::_thesis:_ex_x_being_Element_of_L_st_fq_._k_=_rpoly_(1,x) percases ( k < i or i <= k ) ; supposeH12: k < i ; ::_thesis: ex x being Element of L st fq . k = rpoly (1,x) ex y being Element of L st ( y is_a_common_root_of z `1 ,z `2 & f . k = rpoly (1,y) ) by H13, H1a; hence ex x being Element of L st fq . k = rpoly (1,x) by H12, FINSEQ_3:110; ::_thesis: verum end; supposeH12: i <= k ; ::_thesis: ex x being Element of L st fq . k = rpoly (1,x) ex y being Element of L st ( y is_a_common_root_of z `1 ,z `2 & f . (k + 1) = rpoly (1,y) ) by H1a, H14c; hence ex x being Element of L st fq . k = rpoly (1,x) by H12, H14b, H5, H14, FINSEQ_3:111; ::_thesis: verum end; end; end; hence ex x being Element of L st fq . k = rpoly (1,x) ; ::_thesis: verum end; X101: now__::_thesis:_for_k_being_Nat_st_k_in_dom_gq_holds_ ex_x_being_Element_of_L_st_gq_._k_=_rpoly_(1,x) let k be Nat; ::_thesis: ( k in dom gq implies ex x being Element of L st gq . k = rpoly (1,x) ) assume H11: k in dom gq ; ::_thesis: ex x being Element of L st gq . k = rpoly (1,x) consider m being Nat such that H14: ( len g = m + 1 & len gq = m ) by H6, FINSEQ_3:104; H14a: k in Seg m by H11, H14, FINSEQ_1:def_3; Seg m c= Seg (m + 1) by FINSEQ_3:18; then k in Seg (m + 1) by H14a; then H13: k in dom g by H14, FINSEQ_1:def_3; H14b: k <= m by H14a, FINSEQ_1:1; then H14d: k + 1 <= m + 1 by XREAL_1:6; 1 <= k + 1 by NAT_1:11; then k + 1 in Seg (m + 1) by H14d; then H14c: k + 1 in dom g by H14, FINSEQ_1:def_3; now__::_thesis:_ex_x_being_Element_of_L_st_gq_._k_=_rpoly_(1,x) percases ( k < j or j <= k ) ; supposeH12: k < j ; ::_thesis: ex x being Element of L st gq . k = rpoly (1,x) ex y being Element of L st ( y is_a_common_root_of z `1 ,z `2 & g . k = rpoly (1,y) ) by H13, H2a; hence ex x being Element of L st gq . k = rpoly (1,x) by H12, FINSEQ_3:110; ::_thesis: verum end; supposeH12: j <= k ; ::_thesis: ex x being Element of L st gq . k = rpoly (1,x) ex y being Element of L st ( y is_a_common_root_of z `1 ,z `2 & g . (k + 1) = rpoly (1,y) ) by H2a, H14c; hence ex x being Element of L st gq . k = rpoly (1,x) by H12, H14b, H6, H14, FINSEQ_3:111; ::_thesis: verum end; end; end; hence ex x being Element of L st gq . k = rpoly (1,x) ; ::_thesis: verum end; reconsider z2q = Product fq as Polynomial of L by POLYNOM3:def_10; z2q <> 0_. L by X100, div4; then reconsider z2q = z2q as non zero Polynomial of L by defzer; reconsider g2q = Product gq as Polynomial of L by POLYNOM3:def_10; g2q <> 0_. L by X101, div4; then reconsider g2q = g2q as non zero Polynomial of L by defzer; H7: Product f = (f /. i) * (Product fq) by H5, del1; H7a: Product g = (g /. j) * (Product gq) by H6, del1; Seg (len f) = dom f by FINSEQ_1:def_3; then ( 1 <= i & i <= len f ) by H5, FINSEQ_1:1; then f /. i = rpoly (1,x) by H5, FINSEQ_4:15; then H9: (rpoly (1,x)) *' z2q = Product f by H7, POLYNOM3:def_10; then H8: (rpoly (1,x)) *' (z2q *' (z1 `1)) = z2 *' (z1 `1) by H1a, POLYNOM3:33 .= (rpoly (1,x)) *' q1 by HX, H1, XTUPLE_0:def_2 .= (rpoly (1,x)) *' (q `1) by XTUPLE_0:def_2 ; then H8b: z2q *' (z1 `1) = q `1 by thequiv1; H8a: (rpoly (1,x)) *' (z2q *' (z1 `2)) = z2 *' (z1 `2) by H9, H1a, POLYNOM3:33 .= (rpoly (1,x)) *' q2 by HY, H1, XTUPLE_0:def_3 .= (rpoly (1,x)) *' (q `2) by XTUPLE_0:def_3 ; then z2q *' (z1 `2) = q `2 by thequiv1; then I1: q = [(z2q *' (z1 `1)),(z2q *' (z1 `2))] by H8b, MCART_1:8; I3: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_fq_holds_ ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_q_`1_,q_`2_&_fq_._k_=_rpoly_(1,x)_) let k be Element of NAT ; ::_thesis: ( k in dom fq implies ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) ) assume H11: k in dom fq ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) consider m being Nat such that H14: ( len f = m + 1 & len fq = m ) by H5, FINSEQ_3:104; H14a: k in Seg m by H11, H14, FINSEQ_1:def_3; Seg m c= Seg (m + 1) by FINSEQ_3:18; then k in Seg (m + 1) by H14a; then H13: k in dom f by H14, FINSEQ_1:def_3; H14b: k <= m by H14a, FINSEQ_1:1; then H14d: k + 1 <= m + 1 by XREAL_1:6; 1 <= k + 1 by NAT_1:11; then k + 1 in Seg (m + 1) by H14d; then H14c: k + 1 in dom f by H14, FINSEQ_1:def_3; now__::_thesis:_ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_q_`1_,q_`2_&_fq_._k_=_rpoly_(1,x)_) percases ( k < i or i <= k ) ; supposeH12: k < i ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) then H12a: f . k = fq . k by FINSEQ_3:110; consider y being Element of L such that H10: ( y is_a_common_root_of z `1 ,z `2 & f . k = rpoly (1,y) ) by H13, H1a; H25: eval (z2q,y) = 0. L by H12a, H10, H11, X100, div2; then 0. L = (eval (z2q,y)) * (eval ((z1 `1),y)) by VECTSP_1:7 .= eval ((z2q *' (z1 `1)),y) by POLYNOM4:24 .= eval ((q `1),y) by H8, thequiv1 ; then A1: y is_a_root_of q `1 by POLYNOM5:def_6; 0. L = (eval (z2q,y)) * (eval ((z1 `2),y)) by VECTSP_1:7, H25 .= eval ((z2q *' (z1 `2)),y) by POLYNOM4:24 .= eval ((q `2),y) by H8a, thequiv1 ; then y is_a_root_of q `2 by POLYNOM5:def_6; then y is_a_common_root_of q `1 ,q `2 by A1, root1; hence ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) by H10, H12, FINSEQ_3:110; ::_thesis: verum end; supposeH12: i <= k ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) then H12a: f . (k + 1) = fq . k by H14b, H5, H14, FINSEQ_3:111; consider y being Element of L such that H10: ( y is_a_common_root_of z `1 ,z `2 & f . (k + 1) = rpoly (1,y) ) by H1a, H14c; H25: eval (z2q,y) = 0. L by H12a, H10, H11, X100, div2; then 0. L = (eval (z2q,y)) * (eval ((z1 `1),y)) by VECTSP_1:7 .= eval ((z2q *' (z1 `1)),y) by POLYNOM4:24 .= eval ((q `1),y) by H8, thequiv1 ; then A1: y is_a_root_of q `1 by POLYNOM5:def_6; 0. L = (eval (z2q,y)) * (eval ((z1 `2),y)) by VECTSP_1:7, H25 .= eval ((z2q *' (z1 `2)),y) by POLYNOM4:24 .= eval ((q `2),y) by H8a, thequiv1 ; then y is_a_root_of q `2 by POLYNOM5:def_6; then y is_a_common_root_of q `1 ,q `2 by A1, root1; hence ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) by H10, H12, H14b, H5, H14, FINSEQ_3:111; ::_thesis: verum end; end; end; hence ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) ; ::_thesis: verum end; Seg (len g) = dom g by FINSEQ_1:def_3; then ( 1 <= j & j <= len g ) by H6, FINSEQ_1:1; then g /. j = rpoly (1,x) by H6, FINSEQ_4:15; then H9: (rpoly (1,x)) *' g2q = Product g by H7a, POLYNOM3:def_10; then H8: (rpoly (1,x)) *' (g2q *' (g1 `1)) = g2 *' (g1 `1) by H2a, POLYNOM3:33 .= z `1 by H2, XTUPLE_0:def_2 .= (rpoly (1,x)) *' (q `1) by HX, XTUPLE_0:def_2 ; then H8b: g2q *' (g1 `1) = q `1 by thequiv1; H8a: (rpoly (1,x)) *' (g2q *' (g1 `2)) = g2 *' (g1 `2) by H9, H2a, POLYNOM3:33 .= z `2 by H2, XTUPLE_0:def_3 .= (rpoly (1,x)) *' (q `2) by HY, XTUPLE_0:def_3 ; then g2q *' (g1 `2) = q `2 by thequiv1; then I2: q = [(g2q *' (g1 `1)),(g2q *' (g1 `2))] by H8b, MCART_1:8; I4: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_gq_holds_ ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_q_`1_,q_`2_&_gq_._k_=_rpoly_(1,x)_) let k be Element of NAT ; ::_thesis: ( k in dom gq implies ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) ) assume H11: k in dom gq ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) consider m being Nat such that H14: ( len g = m + 1 & len gq = m ) by H6, FINSEQ_3:104; H14a: k in Seg m by H11, H14, FINSEQ_1:def_3; Seg m c= Seg (m + 1) by FINSEQ_3:18; then k in Seg (m + 1) by H14a; then H13: k in dom g by H14, FINSEQ_1:def_3; H14b: k <= m by H14a, FINSEQ_1:1; then H14d: k + 1 <= m + 1 by XREAL_1:6; 1 <= k + 1 by NAT_1:11; then k + 1 in Seg (m + 1) by H14d; then H14c: k + 1 in dom g by H14, FINSEQ_1:def_3; now__::_thesis:_ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_q_`1_,q_`2_&_gq_._k_=_rpoly_(1,x)_) percases ( k < j or j <= k ) ; supposeH12: k < j ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) then H12a: g . k = gq . k by FINSEQ_3:110; consider y being Element of L such that H10: ( y is_a_common_root_of z `1 ,z `2 & g . k = rpoly (1,y) ) by H13, H2a; H25: eval (g2q,y) = 0. L by H12a, H10, H11, X101, div2; then 0. L = (eval (g2q,y)) * (eval ((g1 `1),y)) by VECTSP_1:7 .= eval ((g2q *' (g1 `1)),y) by POLYNOM4:24 .= eval ((q `1),y) by H8, thequiv1 ; then A1: y is_a_root_of q `1 by POLYNOM5:def_6; 0. L = (eval (g2q,y)) * (eval ((g1 `2),y)) by VECTSP_1:7, H25 .= eval ((g2q *' (g1 `2)),y) by POLYNOM4:24 .= eval ((q `2),y) by H8a, thequiv1 ; then y is_a_root_of q `2 by POLYNOM5:def_6; then y is_a_common_root_of q `1 ,q `2 by A1, root1; hence ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) by H10, H12, FINSEQ_3:110; ::_thesis: verum end; supposeH12: j <= k ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) then H13: g . (k + 1) = gq . k by H14b, H6, H14, FINSEQ_3:111; consider y being Element of L such that H10: ( y is_a_common_root_of z `1 ,z `2 & g . (k + 1) = rpoly (1,y) ) by H2a, H14c; H25: eval (g2q,y) = 0. L by H13, H10, H11, X101, div2; then 0. L = (eval (g2q,y)) * (eval ((g1 `1),y)) by VECTSP_1:7 .= eval ((g2q *' (g1 `1)),y) by POLYNOM4:24 .= eval ((q `1),y) by H8, thequiv1 ; then A1: y is_a_root_of q `1 by POLYNOM5:def_6; 0. L = (eval (g2q,y)) * (eval ((g1 `2),y)) by VECTSP_1:7, H25 .= eval ((g2q *' (g1 `2)),y) by POLYNOM4:24 .= eval ((q `2),y) by H8a, thequiv1 ; then y is_a_root_of q `2 by POLYNOM5:def_6; then y is_a_common_root_of q `1 ,q `2 by A1, root1; hence ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) by H10, H12, H14b, H6, H14, FINSEQ_3:111; ::_thesis: verum end; end; end; hence ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) ; ::_thesis: verum end; thus z1 = g1 by H1, H2, I1, I2, I3, I4, AS2, IV; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS); max ((deg (z `1)),(deg (z `2))) >= deg (z `2) by XXREAL_0:25; then max ((deg (z `1)),(deg (z `2))) >= 0 ; then max ((deg (z `1)),(deg (z `2))) in NAT by INT_1:3; hence z1 = g1 by I, H1, H2; ::_thesis: verum end; definition let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be rational_function of L; func NF z -> rational_function of L means :defNF: :: RATFUNC1:def 17 ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & it = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) if not z is zero otherwise it = 0._ L; existence ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) ) proof percases ( not z is zero or z is zero ) ; suppose not z is zero ; ::_thesis: ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) ) consider z1 being rational_function of L, z2 being non zero Polynomial of L such that H: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by ratfuncNF; reconsider nfz = NormRatF z1 as rational_function of L ; ex zz1 being rational_function of L ex zz2 being non zero Polynomial of L st ( nfz = NormRatF zz1 & zz1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( zz2 = Product f & z = [(zz2 *' (zz1 `1)),(zz2 *' (zz1 `2))] & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by H; hence ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) ) ; ::_thesis: verum end; suppose z is zero ; ::_thesis: ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) ) hence ( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) ) ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being rational_function of L holds ( ( not z is zero & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b2 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) implies b1 = b2 ) & ( z is zero & b1 = 0._ L & b2 = 0._ L implies b1 = b2 ) ) by ratfuncNFunique2; consistency for b1 being rational_function of L holds verum ; end; :: deftheorem defNF defines NF RATFUNC1:def_17_:_ for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z, b3 being rational_function of L holds ( ( not z is zero implies ( b3 = NF z iff ex z1 being rational_function of L ex z2 being non zero Polynomial of L st ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b3 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) ) & ( z is zero implies ( b3 = NF z iff b3 = 0._ L ) ) ); registration let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be rational_function of L; cluster NF z -> irreducible normalized ; coherence ( NF z is normalized & NF z is irreducible ) proof percases ( not z is zero or z is zero ) ; suppose not z is zero ; ::_thesis: ( NF z is normalized & NF z is irreducible ) then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that H: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by defNF; A: NF z is irreducible by H, tw2; (NF z) `2 = ((1. L) / (LC (z1 `2))) * (z1 `2) by H, XTUPLE_0:def_3; hence ( NF z is normalized & NF z is irreducible ) by A, defnorm; ::_thesis: verum end; suppose z is zero ; ::_thesis: ( NF z is normalized & NF z is irreducible ) then NF z = 0._ L by defNF; hence ( NF z is normalized & NF z is irreducible ) ; ::_thesis: verum end; end; end; end; registration let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be non zero rational_function of L; cluster NF z -> non zero ; coherence not NF z is zero proof consider z1 being rational_function of L, z2 being non zero Polynomial of L such that H: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by defNF; now__::_thesis:_not_z1_`1_=_0_._L assume z1 `1 = 0_. L ; ::_thesis: contradiction then 0_. L = z2 *' (z1 `1) by POLYNOM3:34 .= z `1 by H, XTUPLE_0:def_2 ; hence contradiction by defzerrat; ::_thesis: verum end; then not z1 is zero by defzerrat; hence not NF z is zero by H; ::_thesis: verum end; end; defnf1a: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z let z be non zero irreducible rational_function of L; ::_thesis: NF z = NormRationalFunction z consider z1 being rational_function of L, z2 being non zero Polynomial of L such that A1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by defNF; consider f being FinSequence of (Polynom-Ring L) such that A2: ( z2 = Product f & z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by A1; now__::_thesis:_(_f_<>_<*>_the_carrier_of_(Polynom-Ring_L)_implies_for_i_being_Element_of_dom_f_holds_contradiction_) assume AS: f <> <*> the carrier of (Polynom-Ring L) ; ::_thesis: for i being Element of dom f holds contradiction let i be Element of dom f; ::_thesis: contradiction dom f <> {} by AS; then i in dom f ; then reconsider i = i as Element of NAT ; consider x being Element of L such that A4: ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by A2, AS; z `1 ,z `2 have_common_roots by A4, root2; hence contradiction by defirred; ::_thesis: verum end; then A5: Product f = 1_ (Polynom-Ring L) by GROUP_4:8 .= 1_. L by POLYNOM3:def_10 ; then z = [(z1 `1),(z2 *' (z1 `2))] by A2, POLYNOM3:35 .= [(z1 `1),(z1 `2)] by A2, A5, POLYNOM3:35 .= z1 by ttt ; hence NF z = NormRationalFunction z by A1; ::_thesis: verum end; theorem :: RATFUNC1:22 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being non zero rational_function of L for z1 being rational_function of L for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds NF z = NormRationalFunction z1 by defNF; theorem :: RATFUNC1:23 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr holds NF (0._ L) = 0._ L by defNF; theorem :: RATFUNC1:24 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr holds NF (1._ L) = 1._ L proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: NF (1._ L) = 1._ L set z = 1._ L; B: NF (1._ L) = NormRatF (1._ L) by defnf1a .= [(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `1)),(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `2))] ; (1._ L) `2 is normalized by defnorm; then D: LC ((1._ L) `2) = 1. L by defnormp; C: (1. L) / (LC ((1._ L) `2)) = 1. L by D, VECTSP_1:def_10; hence NF (1._ L) = [((1._ L) `1),(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `2))] by B, POLYNOM5:27 .= [((1._ L) `1),((1._ L) `2)] by C, POLYNOM5:27 .= 1._ L by ttt ; ::_thesis: verum end; theorem :: RATFUNC1:25 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z by defnf1a; tt2: for L being non trivial right_complementable unital distributive Abelian add-associative right_zeroed domRing-like left_zeroed doubleLoopStr for p1, p2 being Polynomial of L holds ( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L ) proof let L be non trivial right_complementable unital distributive Abelian add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ; ::_thesis: for p1, p2 being Polynomial of L holds ( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L ) let p1, p2 be Polynomial of L; ::_thesis: ( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L ) assume AS: p1 *' p2 = 0_. L ; ::_thesis: ( p1 = 0_. L or p2 = 0_. L ) now__::_thesis:_(_p1_<>_0_._L_implies_not_p2_<>_0_._L_) assume ( p1 <> 0_. L & p2 <> 0_. L ) ; ::_thesis: contradiction then reconsider x1 = p1, x2 = p2 as non zero Polynomial of L by defzer; not x1 *' x2 is zero ; hence contradiction by AS; ::_thesis: verum end; hence ( p1 = 0_. L or p2 = 0_. L ) ; ::_thesis: verum end; theorem nfequiv: :: RATFUNC1:26 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being rational_function of L for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z let z be rational_function of L; ::_thesis: for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z let x be Element of L; ::_thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z percases ( not z is zero or z is zero ) ; supposeA: not z is zero ; ::_thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that A1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by defNF; consider f being FinSequence of (Polynom-Ring L) such that A2: ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by A1; set q = [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))]; now__::_thesis:_not_[((rpoly_(1,x))_*'_(z_`1)),((rpoly_(1,x))_*'_(z_`2))]_`1_=_0_._L assume [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] `1 = 0_. L ; ::_thesis: contradiction then (rpoly (1,x)) *' (z `1) = 0_. L ; then z `1 = 0_. L by tt2; hence contradiction by A, defzerrat; ::_thesis: verum end; then reconsider q = [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] as non zero rational_function of L by defzerrat; reconsider rp = rpoly (1,x) as Element of (Polynom-Ring L) by POLYNOM3:def_10; set g = <*rp*> ^ f; reconsider g = <*rp*> ^ f as FinSequence of (Polynom-Ring L) ; set g2 = Product g; now__::_thesis:_for_i_being_Nat_st_i_in_dom_g_holds_ ex_z_being_Element_of_L_st_g_._i_=_rpoly_(1,z) let i be Nat; ::_thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) ) assume Y: i in dom g ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z) now__::_thesis:_ex_z_being_Element_of_L_st_g_._i_=_rpoly_(1,z) percases ( i in dom <*rp*> or ex n being Nat st ( n in dom f & i = (len <*rp*>) + n ) ) by Y, FINSEQ_1:25; supposeX: i in dom <*rp*> ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z) then i in {1} by FINSEQ_1:2, FINSEQ_1:38; then i = 1 by TARSKI:def_1; then g . i = <*rp*> . 1 by X, FINSEQ_1:def_7 .= rp by FINSEQ_1:40 ; hence ex z being Element of L st g . i = rpoly (1,z) ; ::_thesis: verum end; suppose ex n being Nat st ( n in dom f & i = (len <*rp*>) + n ) ; ::_thesis: ex z being Element of L st g . i = rpoly (1,z) then consider n being Nat such that H: ( n in dom f & i = (len <*rp*>) + n ) ; J: g . i = f . n by H, FINSEQ_1:def_7; ex x being Element of L st ( x is_a_common_root_of z `1 ,z `2 & f . n = rpoly (1,x) ) by H, A2; hence ex z being Element of L st g . i = rpoly (1,z) by J; ::_thesis: verum end; end; end; hence ex z being Element of L st g . i = rpoly (1,z) ; ::_thesis: verum end; then Product g <> 0_. L by div4; then reconsider g2 = Product g as non zero Polynomial of L by defzer, POLYNOM3:def_10; A3: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_g_holds_ ex_x_being_Element_of_L_st_ (_x_is_a_common_root_of_q_`1_,q_`2_&_g_._i_=_rpoly_(1,x)_) let i be Element of NAT ; ::_thesis: ( i in dom g implies ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) ) ) assume Y: i in dom g ; ::_thesis: ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) ) now__::_thesis:_ex_z_being_Element_of_L_st_ (_z_is_a_common_root_of_q_`1_,q_`2_&_g_._i_=_rpoly_(1,z)_) percases ( i in dom <*rp*> or ex n being Nat st ( n in dom f & i = (len <*rp*>) + n ) ) by Y, FINSEQ_1:25; supposeX: i in dom <*rp*> ; ::_thesis: ex z being Element of L st ( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) then i in {1} by FINSEQ_1:2, FINSEQ_1:38; then i = 1 by TARSKI:def_1; then I: g . i = <*rp*> . 1 by X, FINSEQ_1:def_7 .= rp by FINSEQ_1:40 ; H: eval ((rpoly (1,x)),x) = x - x by HURWITZ:29 .= 0. L by RLVECT_1:15 ; then 0. L = (eval ((rpoly (1,x)),x)) * (eval ((z `1),x)) by VECTSP_1:7 .= eval (((rpoly (1,x)) *' (z `1)),x) by POLYNOM4:24 ; then x is_a_root_of (rpoly (1,x)) *' (z `1) by POLYNOM5:def_6; then J: x is_a_root_of q `1 by XTUPLE_0:def_2; 0. L = (eval ((rpoly (1,x)),x)) * (eval ((z `2),x)) by H, VECTSP_1:7 .= eval (((rpoly (1,x)) *' (z `2)),x) by POLYNOM4:24 ; then x is_a_root_of (rpoly (1,x)) *' (z `2) by POLYNOM5:def_6; then x is_a_root_of q `2 by XTUPLE_0:def_3; then x is_a_common_root_of q `1 ,q `2 by J, root1; hence ex z being Element of L st ( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) by I; ::_thesis: verum end; suppose ex n being Nat st ( n in dom f & i = (len <*rp*>) + n ) ; ::_thesis: ex z being Element of L st ( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) then consider n being Nat such that H: ( n in dom f & i = (len <*rp*>) + n ) ; J: g . i = f . n by H, FINSEQ_1:def_7; consider y being Element of L such that I: ( y is_a_common_root_of z `1 ,z `2 & f . n = rpoly (1,y) ) by H, A2; y is_a_root_of z `1 by I, root1; then eval ((z `1),y) = 0. L by POLYNOM5:def_6; then 0. L = (eval ((rpoly (1,x)),y)) * (eval ((z `1),y)) by VECTSP_1:6 .= eval (((rpoly (1,x)) *' (z `1)),y) by POLYNOM4:24 ; then y is_a_root_of (rpoly (1,x)) *' (z `1) by POLYNOM5:def_6; then K: y is_a_root_of q `1 by XTUPLE_0:def_2; y is_a_root_of z `2 by I, root1; then eval ((z `2),y) = 0. L by POLYNOM5:def_6; then 0. L = (eval ((rpoly (1,x)),y)) * (eval ((z `2),y)) by VECTSP_1:6 .= eval (((rpoly (1,x)) *' (z `2)),y) by POLYNOM4:24 ; then y is_a_root_of (rpoly (1,x)) *' (z `2) by POLYNOM5:def_6; then y is_a_root_of q `2 by XTUPLE_0:def_3; then y is_a_common_root_of q `1 ,q `2 by K, root1; hence ex z being Element of L st ( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) by J, I; ::_thesis: verum end; end; end; hence ex x being Element of L st ( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) ) ; ::_thesis: verum end; A4: Product g = rp * (Product f) by GROUP_4:7; A5: q `1 = (rpoly (1,x)) *' (z `1) by XTUPLE_0:def_2 .= (rpoly (1,x)) *' (z2 *' (z1 `1)) by A1, XTUPLE_0:def_2 .= ((rpoly (1,x)) *' z2) *' (z1 `1) by POLYNOM3:33 .= g2 *' (z1 `1) by A4, A2, POLYNOM3:def_10 ; q `2 = (rpoly (1,x)) *' (z `2) by XTUPLE_0:def_3 .= (rpoly (1,x)) *' (z2 *' (z1 `2)) by A1, XTUPLE_0:def_3 .= ((rpoly (1,x)) *' z2) *' (z1 `2) by POLYNOM3:33 .= g2 *' (z1 `2) by A4, A2, POLYNOM3:def_10 ; then q = [(g2 *' (z1 `1)),(g2 *' (z1 `2))] by A5, ttt; hence NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z by A1, A3, defNF; ::_thesis: verum end; supposeA: z is zero ; ::_thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z then z `1 = 0_. L by defzerrat; then (rpoly (1,x)) *' (z `1) = 0_. L by POLYNOM3:34; then [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] `1 = 0_. L ; then [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] is zero by defzerrat; then NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = 0._ L by defNF; hence NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z by A, defNF; ::_thesis: verum end; end; end; theorem :: RATFUNC1:27 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being rational_function of L holds NF (NF z) = NF z proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L holds NF (NF z) = NF z let z be rational_function of L; ::_thesis: NF (NF z) = NF z set nfz = NF z; percases ( z is zero or not z is zero ) ; suppose z is zero ; ::_thesis: NF (NF z) = NF z then A: NF z = 0._ L by defNF; thus NF (NF z) = NF z by A, defNF; ::_thesis: verum end; supposeA: not z is zero ; ::_thesis: NF (NF z) = NF z H: 1. L <> 0. L ; B: NF (NF z) = NormRatF (NF z) by A, defnf1a .= [(((1. L) / (LC ((NF z) `2))) * ((NF z) `1)),(((1. L) / (LC ((NF z) `2))) * ((NF z) `2))] ; (NF z) `2 is normalized by defnorm; then D: LC ((NF z) `2) = 1. L by defnormp; C: (1. L) / (LC ((NF z) `2)) = 1. L by H, D, VECTSP_1:def_10; then NF (NF z) = [((NF z) `1),(((1. L) / (LC ((NF z) `2))) * ((NF z) `2))] by B, POLYNOM5:27 .= [((NF z) `1),((NF z) `2)] by C, POLYNOM5:27 .= NF z by ttt ; hence NF (NF z) = NF z ; ::_thesis: verum end; end; end; theorem th3: :: RATFUNC1:28 for L being non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being non zero rational_function of L holds ( z is irreducible iff ex a being Element of L st ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ) proof let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being non zero rational_function of L holds ( z is irreducible iff ex a being Element of L st ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ) let z be non zero rational_function of L; ::_thesis: ( z is irreducible iff ex a being Element of L st ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ) set q = z `2 ; set a = (LC (z `2)) " ; now__::_thesis:_not_(LC_(z_`2))_"_=_0._L assume AB: (LC (z `2)) " = 0. L ; ::_thesis: contradiction then AC: ((LC (z `2)) ") * (LC (z `2)) = 0. L by VECTSP_1:7; (LC (z `2)) " <> 1. L by AB; hence contradiction by AC, VECTSP_1:def_10; ::_thesis: verum end; then reconsider a = (LC (z `2)) " as non zero Element of L by STRUCT_0:def_12; reconsider x = [(a * (z `1)),(a * (z `2))] as rational_function of L ; A: now__::_thesis:_(_z_is_irreducible_implies_ex_a_being_Element_of_L_st_ (_a_<>_0._L_&_[(a_*_(z_`1)),(a_*_(z_`2))]_=_NF_z_)_) assume z is irreducible ; ::_thesis: ex a being Element of L st ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) then NF z = NormRatF z by defnf1a .= [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))] ; hence ex a being Element of L st ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ; ::_thesis: verum end; now__::_thesis:_(_ex_a_being_Element_of_L_st_ (_a_<>_0._L_&_[(a_*_(z_`1)),(a_*_(z_`2))]_=_NF_z_)_implies_z_is_irreducible_) assume ex a being Element of L st ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ; ::_thesis: z is irreducible then consider a being Element of L such that H0: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ; reconsider x = [(a * (z `1)),(a * (z `2))] as rational_function of L by H0; H1: ( x `1 = a * (z `1) & x `2 = a * (z `2) ) by XTUPLE_0:def_2, XTUPLE_0:def_3; now__::_thesis:_not_z_`1_,z_`2_have_a_common_root assume z `1 ,z `2 have_a_common_root ; ::_thesis: contradiction then consider u being Element of L such that C1: u is_a_common_root_of z `1 ,z `2 by root2; ( u is_a_root_of z `1 & u is_a_root_of z `2 ) by root1, C1; then C3: ( eval ((z `1),u) = 0. L & eval ((z `2),u) = 0. L ) by POLYNOM5:def_6; eval ((x `1),u) = a * (eval ((z `1),u)) by H1, POLYNOM5:30; then eval ((x `1),u) = 0. L by C3, VECTSP_1:6; then C2: u is_a_root_of x `1 by POLYNOM5:def_6; eval ((x `2),u) = a * (eval ((z `2),u)) by H1, POLYNOM5:30; then eval ((x `2),u) = 0. L by C3, VECTSP_1:7; then u is_a_root_of x `2 by POLYNOM5:def_6; then u is_a_common_root_of x `1 ,x `2 by C2, root1; then x `1 ,x `2 have_a_common_root by root2; hence contradiction by defirred, H0; ::_thesis: verum end; hence z is irreducible by defirred; ::_thesis: verum end; hence ( z is irreducible iff ex a being Element of L st ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ) by A; ::_thesis: verum end; begin definition let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be rational_function of L; func degree z -> Integer equals :: RATFUNC1:def 18 max ((degree ((NF z) `1)),(degree ((NF z) `2))); coherence max ((degree ((NF z) `1)),(degree ((NF z) `2))) is Integer ; end; :: deftheorem defines degree RATFUNC1:def_18_:_ for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being rational_function of L holds degree z = max ((degree ((NF z) `1)),(degree ((NF z) `2))); notation let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; let z be rational_function of L; synonym deg z for degree z; end; th1a: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being non zero rational_function of L st z is irreducible holds degree z = max ((degree (z `1)),(degree (z `2))) proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being non zero rational_function of L st z is irreducible holds degree z = max ((degree (z `1)),(degree (z `2))) let z be non zero rational_function of L; ::_thesis: ( z is irreducible implies degree z = max ((degree (z `1)),(degree (z `2))) ) assume z is irreducible ; ::_thesis: degree z = max ((degree (z `1)),(degree (z `2))) then consider a being Element of L such that H: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) by th3; not a is zero by H, STRUCT_0:def_12; then reconsider az2 = a * (z `2) as non zero Polynomial of L ; H3: (NF z) `2 = a * (z `2) by H, XTUPLE_0:def_3; thus degree z = max ((deg (a * (z `1))),(deg (a * (z `2)))) by H, XTUPLE_0:def_2, H3 .= max ((deg (z `1)),(deg az2)) by H, POLYNOM5:25 .= max ((degree (z `1)),(degree (z `2))) by H, POLYNOM5:25 ; ::_thesis: verum end; theorem th1: :: RATFUNC1:29 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being rational_function of L holds degree z <= max ((degree (z `1)),(degree (z `2))) proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being rational_function of L holds degree z <= max ((degree (z `1)),(degree (z `2))) let z be rational_function of L; ::_thesis: degree z <= max ((degree (z `1)),(degree (z `2))) percases ( z is zero or not z is zero ) ; supposeH: z is zero ; ::_thesis: degree z <= max ((degree (z `1)),(degree (z `2))) then A: NF z = 0._ L by defNF .= [(0_. L),(1_. L)] ; z `1 = 0_. L by H, defzerrat; then B: deg (z `1) = - 1 by HURWITZ:20; E: deg (1_. L) = 1 - 1 by POLYNOM4:4; deg z = max ((deg (0_. L)),(degree ((NF z) `2))) by A, XTUPLE_0:def_2 .= max ((deg (0_. L)),(deg (1_. L))) by A, XTUPLE_0:def_3 .= max ((- 1),(deg (1_. L))) by HURWITZ:20 .= 0 by E, XXREAL_0:def_10 ; hence degree z <= max ((degree (z `1)),(degree (z `2))) by B, XXREAL_0:def_10; ::_thesis: verum end; supposeA: not z is zero ; ::_thesis: degree z <= max ((degree (z `1)),(degree (z `2))) defpred S1[ Nat] means for z being non zero rational_function of L st max ((degree (z `1)),(degree (z `2))) = $1 holds max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))); now__::_thesis:_for_z_being_non_zero_rational_function_of_L for_z1_being_rational_function_of_L for_z2_being_non_zero_Polynomial_of_L for_f_being_FinSequence_of_(Polynom-Ring_L)_st_max_((degree_(z_`1)),(degree_(z_`2)))_=_0_holds_ max_((degree_((NF_z)_`1)),(degree_((NF_z)_`2)))_<=_max_((degree_(z_`1)),(degree_(z_`2))) let z be non zero rational_function of L; ::_thesis: for z1 being rational_function of L for z2 being non zero Polynomial of L for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) let z1 be rational_function of L; ::_thesis: for z2 being non zero Polynomial of L for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) let z2 be non zero Polynomial of L; ::_thesis: for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) let f be FinSequence of (Polynom-Ring L); ::_thesis: ( max ((degree (z `1)),(degree (z `2))) = 0 implies max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) ) assume AS: max ((degree (z `1)),(degree (z `2))) = 0 ; ::_thesis: max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) now__::_thesis:_z_`1_,z_`2_have_no_common_roots percases ( degree (z `1) = 0 or degree (z `2) = 0 ) by AS, XXREAL_0:16; supposeH: degree (z `1) = 0 ; ::_thesis: z `1 ,z `2 have_no_common_roots now__::_thesis:_not_z_`1_,z_`2_have_common_roots assume z `1 ,z `2 have_common_roots ; ::_thesis: contradiction then consider x being Element of L such that HH: x is_a_common_root_of z `1 ,z `2 by root2; x is_a_root_of z `1 by HH, root1; then z `1 is with_roots by POLYNOM5:def_7; hence contradiction by HURWITZ:24, H; ::_thesis: verum end; hence z `1 ,z `2 have_no_common_roots ; ::_thesis: verum end; supposeH: degree (z `2) = 0 ; ::_thesis: z `1 ,z `2 have_no_common_roots now__::_thesis:_not_z_`1_,z_`2_have_common_roots assume z `1 ,z `2 have_common_roots ; ::_thesis: contradiction then consider x being Element of L such that HH: x is_a_common_root_of z `1 ,z `2 by root2; x is_a_root_of z `2 by HH, root1; then z `2 is with_roots by POLYNOM5:def_7; hence contradiction by HURWITZ:24, H; ::_thesis: verum end; hence z `1 ,z `2 have_no_common_roots ; ::_thesis: verum end; end; end; then z is irreducible by defirred; then degree z = max ((degree (z `1)),(degree (z `2))) by th1a; hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) ; ::_thesis: verum end; then IA: S1[ 0 ] ; IS: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume IV: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_z_being_non_zero_rational_function_of_L_st_max_((degree_(z_`1)),(degree_(z_`2)))_=_n_+_1_holds_ max_((degree_((NF_z)_`1)),(degree_((NF_z)_`2)))_<=_max_((degree_(z_`1)),(degree_(z_`2))) let z be non zero rational_function of L; ::_thesis: ( max ((degree (z `1)),(degree (z `2))) = n + 1 implies max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2))) ) assume AS: max ((degree (z `1)),(degree (z `2))) = n + 1 ; ::_thesis: max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2))) percases ( z is irreducible or z is reducible ) ; suppose z is irreducible ; ::_thesis: max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2))) then degree z = max ((degree (z `1)),(degree (z `2))) by th1a; hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) ; ::_thesis: verum end; suppose z is reducible ; ::_thesis: max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2))) then z `1 ,z `2 have_common_roots by defirred; then consider x being Element of L such that H: x is_a_common_root_of z `1 ,z `2 by root2; H3: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by H, root1; consider q2 being Polynomial of L such that HY: z `2 = (rpoly (1,x)) *' q2 by H3, HURWITZ:33; consider q1 being Polynomial of L such that HX: z `1 = (rpoly (1,x)) *' q1 by H3, HURWITZ:33; q1 <> 0_. L by defzerrat, HX, POLYNOM3:34; then reconsider q1 = q1 as non zero Polynomial of L by defzer; q2 <> 0_. L by HY, POLYNOM3:34; then reconsider q2 = q2 as non zero Polynomial of L by defzer; set q = [q1,q2]; now__::_thesis:_not_[q1,q2]_is_zero assume [q1,q2] is zero ; ::_thesis: contradiction then [q1,q2] `1 = 0_. L by defzerrat; hence contradiction ; ::_thesis: verum end; then reconsider q = [q1,q2] as non zero rational_function of L ; z = [((rpoly (1,x)) *' q1),((rpoly (1,x)) *' q2)] by ttt, HX, HY .= [((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' q2)] by XTUPLE_0:def_2 .= [((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' (q `2))] by XTUPLE_0:def_3 ; then HZ: NF z = NF q by nfequiv; HV: n <= n + 1 by NAT_1:11; W4: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23 .= 1 + (deg q1) by HURWITZ:27 .= 1 + (deg (q `1)) by XTUPLE_0:def_2 ; deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by HY, HURWITZ:23 .= 1 + (deg q2) by HURWITZ:27 .= 1 + (deg (q `2)) by XTUPLE_0:def_3 ; then HU: max ((degree (z `1)),(degree (z `2))) = 1 + (max ((degree (q `1)),(degree (q `2)))) by W4, maxx; then max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (q `1)),(degree (q `2))) by IV, HZ, AS; hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) by HV, HU, AS, XXREAL_0:2; ::_thesis: verum end; end; end; hence S1[n + 1] ; ::_thesis: verum end; I: for n being Nat holds S1[n] from NAT_1:sch_2(IA, IS); max ((degree (z `1)),(degree (z `2))) >= 0 by XXREAL_0:25; then max ((degree (z `1)),(degree (z `2))) in NAT by INT_1:3; hence degree z <= max ((degree (z `1)),(degree (z `2))) by A, I; ::_thesis: verum end; end; end; theorem :: RATFUNC1:30 for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for z being non zero rational_function of L holds ( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) ) proof let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for z being non zero rational_function of L holds ( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) ) let z be non zero rational_function of L; ::_thesis: ( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) ) set p1 = z `1 ; set p2 = z `2 ; A: now__::_thesis:_(_z_is_irreducible_implies_degree_z_=_max_((degree_(z_`1)),(degree_(z_`2)))_) assume z is irreducible ; ::_thesis: degree z = max ((degree (z `1)),(degree (z `2))) then consider a being Element of L such that A1: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) by th3; A2: degree (a * (z `1)) = degree (z `1) by POLYNOM5:25, A1; A3: degree (a * (z `2)) = degree (z `2) by POLYNOM5:25, A1; degree ((NF z) `1) = degree (z `1) by A2, A1, XTUPLE_0:def_2; hence degree z = max ((degree (z `1)),(degree (z `2))) by A3, A1, XTUPLE_0:def_3; ::_thesis: verum end; now__::_thesis:_(_degree_z_=_max_((degree_(z_`1)),(degree_(z_`2)))_implies_z_is_irreducible_) assume AS: degree z = max ((degree (z `1)),(degree (z `2))) ; ::_thesis: z is irreducible now__::_thesis:_z_is_irreducible assume not z is irreducible ; ::_thesis: contradiction then z `1 ,z `2 have_a_common_root by defirred; then consider x being Element of L such that A1: x is_a_common_root_of z `1 ,z `2 by root2; A2: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by A1, root1; then consider q1 being Polynomial of L such that A3: z `1 = (rpoly (1,x)) *' q1 by HURWITZ:33; consider q2 being Polynomial of L such that A4: z `2 = (rpoly (1,x)) *' q2 by A2, HURWITZ:33; q2 <> 0_. L by A4, POLYNOM3:34; then reconsider q2 = q2 as non zero Polynomial of L by defzer; set zz = [q1,q2]; H1: ( [q1,q2] `1 = q1 & [q1,q2] `2 = q2 ) ; z = [((rpoly (1,x)) *' ([q1,q2] `1)),((rpoly (1,x)) *' ([q1,q2] `2))] by ttt, A3, A4; then NF z = NF [q1,q2] by nfequiv; then degree z = degree [q1,q2] ; then A8: degree z <= max ((degree q1),(degree q2)) by th1, H1; now__::_thesis:_contradiction percases ( z `1 = 0_. L or z `1 <> 0_. L ) ; supposeB0: z `1 = 0_. L ; ::_thesis: contradiction B4: q1 = 0_. L by B0, A3, tt2; (deg ((rpoly (1,x)) *' q2)) + 0 = (deg (rpoly (1,x))) + (deg q2) by HURWITZ:23 .= 1 + (deg q2) by HURWITZ:27 ; then C: deg q2 < deg (z `2) by A4, XREAL_1:8; deg (z `1) <= deg (z `2) by HURWITZ:20, B0; then B3: max ((deg (z `1)),(deg (z `2))) = deg (z `2) by XXREAL_0:def_10; deg q1 <= deg q2 by HURWITZ:20, B4; hence contradiction by B3, C, AS, A8, XXREAL_0:def_10; ::_thesis: verum end; suppose z `1 <> 0_. L ; ::_thesis: contradiction then reconsider p1 = z `1 as non zero Polynomial of L by defzer; now__::_thesis:_not_q1_=_0_._L assume q1 = 0_. L ; ::_thesis: contradiction then p1 = 0_. L by A3, POLYNOM3:34; hence contradiction ; ::_thesis: verum end; then reconsider q1 = q1 as non zero Polynomial of L by defzer; (deg p1) + 0 = (deg (rpoly (1,x))) + (deg q1) by A3, HURWITZ:23 .= 1 + (deg q1) by HURWITZ:27 ; then H2: deg q1 < deg p1 by XREAL_1:8; (deg (z `2)) + 0 = (deg (rpoly (1,x))) + (deg q2) by A4, HURWITZ:23 .= 1 + (deg q2) by HURWITZ:27 ; then deg q2 < deg (z `2) by XREAL_1:8; hence contradiction by AS, A8, H2, XXREAL_0:27; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence z is irreducible ; ::_thesis: verum end; hence ( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) ) by A; ::_thesis: verum end; begin definition let L be Field; let z be rational_function of L; let x be Element of L; func eval (z,x) -> Element of L equals :: RATFUNC1:def 19 (eval ((z `1),x)) / (eval ((z `2),x)); coherence (eval ((z `1),x)) / (eval ((z `2),x)) is Element of L ; end; :: deftheorem defines eval RATFUNC1:def_19_:_ for L being Field for z being rational_function of L for x being Element of L holds eval (z,x) = (eval ((z `1),x)) / (eval ((z `2),x)); theorem ev0: :: RATFUNC1:31 for L being Field for x being Element of L holds eval ((0._ L),x) = 0. L proof let L be Field; ::_thesis: for x being Element of L holds eval ((0._ L),x) = 0. L let x be Element of L; ::_thesis: eval ((0._ L),x) = 0. L thus eval ((0._ L),x) = (eval ((0_. L),x)) * ((eval (((0._ L) `2),x)) ") by XTUPLE_0:def_2 .= (0. L) * ((eval (((0._ L) `2),x)) ") by POLYNOM4:17 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; theorem :: RATFUNC1:32 for L being Field for x being Element of L holds eval ((1._ L),x) = 1. L proof let L be Field; ::_thesis: for x being Element of L holds eval ((1._ L),x) = 1. L let x be Element of L; ::_thesis: eval ((1._ L),x) = 1. L A: 1. L <> 0. L ; thus eval ((1._ L),x) = (eval ((1_. L),x)) * ((eval (((1._ L) `2),x)) ") by XTUPLE_0:def_2 .= (1. L) * ((eval (((1._ L) `2),x)) ") by POLYNOM4:18 .= (1. L) * ((eval ((1_. L),x)) ") by XTUPLE_0:def_3 .= (1. L) * ((1. L) ") by POLYNOM4:18 .= 1. L by A, VECTSP_1:def_10 ; ::_thesis: verum end; theorem :: RATFUNC1:33 for L being Field for p, q being rational_function of L for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) proof let L be Field; ::_thesis: for p, q being rational_function of L for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) let p, q be rational_function of L; ::_thesis: for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) let x be Element of L; ::_thesis: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L implies eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) ) assume AS: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L ) ; ::_thesis: eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) thus eval ((p + q),x) = (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * ((eval (((p + q) `2),x)) ") by XTUPLE_0:def_2 .= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * ((eval (((p `2) *' (q `2)),x)) ") by XTUPLE_0:def_3 .= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * (((eval ((p `2),x)) * (eval ((q `2),x))) ") by POLYNOM4:24 .= (eval ((((p `1) *' (q `2)) + ((p `2) *' (q `1))),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by AS, VECTSP_2:11 .= ((eval (((p `1) *' (q `2)),x)) + (eval (((p `2) *' (q `1)),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by POLYNOM4:19 .= ((eval (((p `1) *' (q `2)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by VECTSP_1:def_3 .= (((eval ((p `1),x)) * (eval ((q `2),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by POLYNOM4:24 .= ((eval ((p `1),x)) * ((eval ((q `2),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by GROUP_1:def_3 .= ((eval ((p `1),x)) * (((eval ((q `2),x)) * ((eval ((q `2),x)) ")) * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by GROUP_1:def_3 .= ((eval ((p `1),x)) * ((1. L) * ((eval ((p `2),x)) "))) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by AS, VECTSP_1:def_10 .= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval (((p `2) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by VECTSP_1:def_8 .= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + (((eval ((p `2),x)) * (eval ((q `1),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by POLYNOM4:24 .= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * ((eval ((p `2),x)) * (((eval ((p `2),x)) ") * ((eval ((q `2),x)) ")))) by GROUP_1:def_3 .= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * (((eval ((p `2),x)) * ((eval ((p `2),x)) ")) * ((eval ((q `2),x)) "))) by GROUP_1:def_3 .= ((eval ((p `1),x)) * ((eval ((p `2),x)) ")) + ((eval ((q `1),x)) * ((1. L) * ((eval ((q `2),x)) "))) by AS, VECTSP_1:def_10 .= (eval (p,x)) + (eval (q,x)) by VECTSP_1:def_8 ; ::_thesis: verum end; theorem :: RATFUNC1:34 for L being Field for p, q being rational_function of L for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) proof let L be Field; ::_thesis: for p, q being rational_function of L for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) let p, q be rational_function of L; ::_thesis: for x being Element of L st eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) let x be Element of L; ::_thesis: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L implies eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) ) assume AS: ( eval ((p `2),x) <> 0. L & eval ((q `2),x) <> 0. L ) ; ::_thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) thus eval ((p *' q),x) = (eval (((p `1) *' (q `1)),x)) * ((eval (((p *' q) `2),x)) ") by XTUPLE_0:def_2 .= (eval (((p `1) *' (q `1)),x)) * ((eval (((p `2) *' (q `2)),x)) ") by XTUPLE_0:def_3 .= (eval (((p `1) *' (q `1)),x)) * (((eval ((p `2),x)) * (eval ((q `2),x))) ") by POLYNOM4:24 .= (eval (((p `1) *' (q `1)),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by AS, VECTSP_2:11 .= ((eval ((p `1),x)) * (eval ((q `1),x))) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) ")) by POLYNOM4:24 .= (eval ((p `1),x)) * ((eval ((q `1),x)) * (((eval ((q `2),x)) ") * ((eval ((p `2),x)) "))) by GROUP_1:def_3 .= (eval ((p `1),x)) * (((eval ((p `2),x)) ") * (((eval ((q `2),x)) ") * (eval ((q `1),x)))) by GROUP_1:def_3 .= (eval (p,x)) * (eval (q,x)) by GROUP_1:def_3 ; ::_thesis: verum end; theorem ev4: :: RATFUNC1:35 for L being Field for p being rational_function of L for x being Element of L st eval ((p `2),x) <> 0. L holds eval ((NormRationalFunction p),x) = eval (p,x) proof let L be Field; ::_thesis: for p being rational_function of L for x being Element of L st eval ((p `2),x) <> 0. L holds eval ((NormRationalFunction p),x) = eval (p,x) let p be rational_function of L; ::_thesis: for x being Element of L st eval ((p `2),x) <> 0. L holds eval ((NormRationalFunction p),x) = eval (p,x) let x be Element of L; ::_thesis: ( eval ((p `2),x) <> 0. L implies eval ((NormRationalFunction p),x) = eval (p,x) ) assume AS: eval ((p `2),x) <> 0. L ; ::_thesis: eval ((NormRationalFunction p),x) = eval (p,x) set np = NormRationalFunction p; H: (1. L) / (LC (p `2)) <> 0. L ; thus eval ((NormRationalFunction p),x) = (eval ((((1. L) / (LC (p `2))) * (p `1)),x)) * ((eval (((NormRationalFunction p) `2),x)) ") by XTUPLE_0:def_2 .= (eval ((((1. L) / (LC (p `2))) * (p `1)),x)) * ((eval ((((1. L) / (LC (p `2))) * (p `2)),x)) ") by XTUPLE_0:def_3 .= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((eval ((((1. L) / (LC (p `2))) * (p `2)),x)) ") by POLYNOM5:30 .= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((((1. L) / (LC (p `2))) * (eval ((p `2),x))) ") by POLYNOM5:30 .= (((1. L) / (LC (p `2))) * (eval ((p `1),x))) * ((((1. L) / (LC (p `2))) ") * ((eval ((p `2),x)) ")) by AS, VECTSP_2:11 .= (eval ((p `1),x)) * (((1. L) / (LC (p `2))) * ((((1. L) / (LC (p `2))) ") * ((eval ((p `2),x)) "))) by GROUP_1:def_3 .= (eval ((p `1),x)) * ((((1. L) / (LC (p `2))) * (((1. L) / (LC (p `2))) ")) * ((eval ((p `2),x)) ")) by GROUP_1:def_3 .= (eval ((p `1),x)) * ((1. L) * ((eval ((p `2),x)) ")) by H, VECTSP_1:def_10 .= eval (p,x) by VECTSP_1:def_8 ; ::_thesis: verum end; theorem :: RATFUNC1:36 for L being Field for p being rational_function of L for x being Element of L holds ( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) ) proof let L be Field; ::_thesis: for p being rational_function of L for x being Element of L holds ( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) ) let p be rational_function of L; ::_thesis: for x being Element of L holds ( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) ) let x be Element of L; ::_thesis: ( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) ) assume AS1: eval ((p `2),x) <> 0. L ; ::_thesis: ( x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) ) assume AS: not x is_a_common_root_of p `1 ,p `2 ; ::_thesis: eval ((NF p),x) = eval (p,x) percases ( p is zero or not p is zero ) ; supposeH: p is zero ; ::_thesis: eval ((NF p),x) = eval (p,x) then H1: p `1 = 0_. L by defzerrat; H2: NF p = 0._ L by H, defNF; thus eval (p,x) = (0. L) * ((eval ((p `2),x)) ") by H1, POLYNOM4:17 .= 0. L by VECTSP_1:7 .= eval ((NF p),x) by H2, ev0 ; ::_thesis: verum end; suppose not p is zero ; ::_thesis: eval ((NF p),x) = eval (p,x) then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that H: ( p = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF p = NormRatF z1 & ex f being FinSequence of (Polynom-Ring L) st ( z2 = Product f & ( for i being Element of NAT st i in dom f holds ex x being Element of L st ( x is_a_common_root_of p `1 ,p `2 & f . i = rpoly (1,x) ) ) ) ) by defNF; H1: p `1 = z2 *' (z1 `1) by H, XTUPLE_0:def_2; H2: p `2 = z2 *' (z1 `2) by H, XTUPLE_0:def_3; H3: now__::_thesis:_not_eval_(z2,x)_=_0._L assume A: eval (z2,x) = 0. L ; ::_thesis: contradiction eval ((z2 *' (z1 `1)),x) = (eval (z2,x)) * (eval ((z1 `1),x)) by POLYNOM4:24 .= 0. L by A, VECTSP_1:7 ; then B: x is_a_root_of p `1 by H1, POLYNOM5:def_6; eval ((z2 *' (z1 `2)),x) = (eval (z2,x)) * (eval ((z1 `2),x)) by POLYNOM4:24 .= 0. L by A, VECTSP_1:7 ; then x is_a_root_of p `2 by H2, POLYNOM5:def_6; hence contradiction by AS, B, root1; ::_thesis: verum end; H6: now__::_thesis:_not_eval_((z1_`2),x)_=_0._L assume eval ((z1 `2),x) = 0. L ; ::_thesis: contradiction then 0. L = (eval (z2,x)) * (eval ((z1 `2),x)) by VECTSP_1:7 .= eval ((z2 *' (z1 `2)),x) by POLYNOM4:24 ; hence contradiction by H, XTUPLE_0:def_3, AS1; ::_thesis: verum end; eval (p,x) = (eval ((z2 *' (z1 `1)),x)) * ((eval ((z2 *' (z1 `2)),x)) ") by H, XTUPLE_0:def_3, H1 .= ((eval (z2,x)) * (eval ((z1 `1),x))) * ((eval ((z2 *' (z1 `2)),x)) ") by POLYNOM4:24 .= ((eval (z2,x)) * (eval ((z1 `1),x))) * (((eval (z2,x)) * (eval ((z1 `2),x))) ") by POLYNOM4:24 .= ((eval (z2,x)) * (eval ((z1 `1),x))) * (((eval ((z1 `2),x)) ") * ((eval (z2,x)) ")) by H3, H6, VECTSP_2:11 .= (eval (z2,x)) * ((eval ((z1 `1),x)) * (((eval ((z1 `2),x)) ") * ((eval (z2,x)) "))) by GROUP_1:def_3 .= (eval (z2,x)) * (((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) * ((eval (z2,x)) ")) by GROUP_1:def_3 .= ((eval (z2,x)) * ((eval (z2,x)) ")) * ((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) by GROUP_1:def_3 .= (1. L) * ((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) by H3, VECTSP_1:def_10 .= eval (z1,x) by VECTSP_1:def_8 ; hence eval ((NF p),x) = eval (p,x) by H, H6, ev4; ::_thesis: verum end; end; end;