:: POLYNOM4 semantic presentation begin theorem :: POLYNOM4:1 for D being non empty set for p being FinSequence of D for n being Element of NAT st 1 <= n & n <= len p holds p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) by FINSEQ_5:84; Lm1: for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr for a being Element of R holds a * (0. R) = 0. R proof let R be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; ::_thesis: for a being Element of R holds a * (0. R) = 0. R let a be Element of R; ::_thesis: a * (0. R) = 0. R a * (0. R) = a * ((0. R) + (0. R)) by ALGSTR_1:def_2 .= (a * (0. R)) + (a * (0. R)) by VECTSP_1:def_2 ; then (a * (0. R)) + (a * (0. R)) = (0. R) + (a * (0. R)) by ALGSTR_1:def_2; hence a * (0. R) = 0. R by ALGSTR_0:def_4; ::_thesis: verum end; registration cluster non empty right_add-cancelable almost_left_invertible associative commutative right-distributive well-unital left_zeroed -> non empty right_add-cancelable associative commutative right-distributive well-unital domRing-like left_zeroed for doubleLoopStr ; coherence for b1 being non empty right_add-cancelable associative commutative right-distributive well-unital left_zeroed doubleLoopStr st b1 is almost_left_invertible holds b1 is domRing-like proof let L be non empty right_add-cancelable associative commutative right-distributive well-unital left_zeroed doubleLoopStr ; ::_thesis: ( L is almost_left_invertible implies L is domRing-like ) assume A1: L is almost_left_invertible ; ::_thesis: L is domRing-like now__::_thesis:_for_x,_y_being_Element_of_L_holds_ (_not_x_*_y_=_0._L_or_x_=_0._L_or_y_=_0._L_) let x, y be Element of L; ::_thesis: ( not x * y = 0. L or x = 0. L or y = 0. L ) assume A2: x * y = 0. L ; ::_thesis: ( x = 0. L or y = 0. L ) thus ( x = 0. L or y = 0. L ) ::_thesis: verum proof assume x <> 0. L ; ::_thesis: y = 0. L then consider z being Element of L such that A3: z * x = 1. L by A1, VECTSP_1:def_9; z * (0. L) = (1. L) * y by A2, A3, GROUP_1:def_3 .= y by VECTSP_1:def_8 ; hence y = 0. L by Lm1; ::_thesis: verum end; end; hence L is domRing-like by VECTSP_2:def_1; ::_thesis: verum end; end; registration cluster non empty non degenerated non trivial right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital associative commutative distributive domRing-like for doubleLoopStr ; existence ex b1 being non trivial doubleLoopStr st ( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is distributive & b1 is unital & b1 is domRing-like & b1 is almost_left_invertible & not b1 is degenerated ) proof set F = the strict Field; take the strict Field ; ::_thesis: ( the strict Field is strict & the strict Field is Abelian & the strict Field is add-associative & the strict Field is right_zeroed & the strict Field is right_complementable & the strict Field is associative & the strict Field is commutative & the strict Field is distributive & the strict Field is unital & the strict Field is domRing-like & the strict Field is almost_left_invertible & not the strict Field is degenerated ) thus ( the strict Field is strict & the strict Field is Abelian & the strict Field is add-associative & the strict Field is right_zeroed & the strict Field is right_complementable & the strict Field is associative & the strict Field is commutative & the strict Field is distributive & the strict Field is unital & the strict Field is domRing-like & the strict Field is almost_left_invertible & not the strict Field is degenerated ) ; ::_thesis: verum end; end; begin theorem Th2: :: POLYNOM4:2 for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr for p being sequence of L holds (0_. L) *' p = 0_. L proof let L be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for p being sequence of L holds (0_. L) *' p = 0_. L let p be sequence of L; ::_thesis: (0_. L) *' p = 0_. L now__::_thesis:_for_i_being_Element_of_NAT_holds_((0_._L)_*'_p)_._i_=_(0_._L)_._i let i be Element of NAT ; ::_thesis: ((0_. L) *' p) . i = (0_. L) . i consider r being FinSequence of the carrier of L such that len r = i + 1 and A1: ((0_. L) *' p) . i = Sum r and A2: for k being Element of NAT st k in dom r holds r . k = ((0_. L) . (k -' 1)) * (p . ((i + 1) -' k)) by POLYNOM3:def_9; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_ r_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom r implies r . k = 0. L ) assume k in dom r ; ::_thesis: r . k = 0. L hence r . k = ((0_. L) . (k -' 1)) * (p . ((i + 1) -' k)) by A2 .= (0. L) * (p . ((i + 1) -' k)) by FUNCOP_1:7 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; hence ((0_. L) *' p) . i = 0. L by A1, POLYNOM3:1 .= (0_. L) . i by FUNCOP_1:7 ; ::_thesis: verum end; hence (0_. L) *' p = 0_. L by FUNCT_2:63; ::_thesis: verum end; theorem Th3: :: POLYNOM4:3 for L being non empty ZeroStr holds len (0_. L) = 0 proof let L be non empty ZeroStr ; ::_thesis: len (0_. L) = 0 now__::_thesis:_for_i_being_Nat_st_i_>=_0_holds_ (0_._L)_._i_=_0._L let i be Nat; ::_thesis: ( i >= 0 implies (0_. L) . i = 0. L ) i in NAT by ORDINAL1:def_12; hence ( i >= 0 implies (0_. L) . i = 0. L ) by FUNCOP_1:7; ::_thesis: verum end; then 0 is_at_least_length_of 0_. L by ALGSEQ_1:def_2; hence len (0_. L) = 0 by ALGSEQ_1:def_3; ::_thesis: verum end; theorem Th4: :: POLYNOM4:4 for L being non empty non degenerated multLoopStr_0 holds len (1_. L) = 1 proof let L be non empty non degenerated multLoopStr_0 ; ::_thesis: len (1_. L) = 1 A1: now__::_thesis:_for_i_being_Nat_st_i_is_at_least_length_of_1_._L_holds_ not_0_+_1_>_i let i be Nat; ::_thesis: ( i is_at_least_length_of 1_. L implies not 0 + 1 > i ) assume that A2: i is_at_least_length_of 1_. L and A3: 0 + 1 > i ; ::_thesis: contradiction 0 >= i by A3, NAT_1:13; then (1_. L) . 0 = 0. L by A2, ALGSEQ_1:def_2; hence contradiction by POLYNOM3:30; ::_thesis: verum end; for i being Nat st i >= 1 holds (1_. L) . i = 0. L by POLYNOM3:30; then 1 is_at_least_length_of 1_. L by ALGSEQ_1:def_2; hence len (1_. L) = 1 by A1, ALGSEQ_1:def_3; ::_thesis: verum end; theorem Th5: :: POLYNOM4:5 for L being non empty ZeroStr for p being Polynomial of L st len p = 0 holds p = 0_. L proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L st len p = 0 holds p = 0_. L let p be Polynomial of L; ::_thesis: ( len p = 0 implies p = 0_. L ) assume len p = 0 ; ::_thesis: p = 0_. L then A1: 0 is_at_least_length_of p by ALGSEQ_1:def_3; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_p_holds_ p_._x_=_0._L let x be set ; ::_thesis: ( x in dom p implies p . x = 0. L ) assume x in dom p ; ::_thesis: p . x = 0. L then reconsider i = x as Element of NAT by NORMSP_1:12; i >= 0 ; hence p . x = 0. L by A1, ALGSEQ_1:def_2; ::_thesis: verum end; dom p = NAT by NORMSP_1:12; hence p = 0_. L by A2, FUNCOP_1:11; ::_thesis: verum end; theorem Th6: :: POLYNOM4:6 for L being non empty right_zeroed addLoopStr for p, q being Polynomial of L for n being Element of NAT st n >= len p & n >= len q holds n >= len (p + q) proof let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of L for n being Element of NAT st n >= len p & n >= len q holds n >= len (p + q) let p, q be Polynomial of L; ::_thesis: for n being Element of NAT st n >= len p & n >= len q holds n >= len (p + q) let n be Element of NAT ; ::_thesis: ( n >= len p & n >= len q implies n >= len (p + q) ) assume ( n >= len p & n >= len q ) ; ::_thesis: n >= len (p + q) then ( n is_at_least_length_of p & n is_at_least_length_of q ) by POLYNOM3:23; then n is_at_least_length_of p + q by POLYNOM3:24; hence n >= len (p + q) by POLYNOM3:23; ::_thesis: verum end; theorem Th7: :: POLYNOM4:7 for L being non empty right_complementable add-associative right_zeroed addLoopStr for p, q being Polynomial of L st len p <> len q holds len (p + q) = max ((len p),(len q)) proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of L st len p <> len q holds len (p + q) = max ((len p),(len q)) let p, q be Polynomial of L; ::_thesis: ( len p <> len q implies len (p + q) = max ((len p),(len q)) ) assume A1: len p <> len q ; ::_thesis: len (p + q) = max ((len p),(len q)) percases ( len p < len q or len p > len q ) by A1, XXREAL_0:1; supposeA2: len p < len q ; ::_thesis: len (p + q) = max ((len p),(len q)) then len q >= (len p) + 1 by NAT_1:13; then (len q) - 1 >= len p by XREAL_1:19; then A3: (len q) -' 1 >= len p by XREAL_0:def_2; len q >= 0 + 1 by A2, NAT_1:13; then A4: len q = ((len q) -' 1) + 1 by XREAL_1:235; A5: (p + q) . ((len q) -' 1) = (p . ((len q) -' 1)) + (q . ((len q) -' 1)) by NORMSP_1:def_2 .= (0. L) + (q . ((len q) -' 1)) by A3, ALGSEQ_1:8 .= q . ((len q) -' 1) by RLVECT_1:4 ; A6: len (p + q) >= len q proof assume len (p + q) < len q ; ::_thesis: contradiction then (len (p + q)) + 1 <= len q by NAT_1:13; then len (p + q) <= (len q) - 1 by XREAL_1:19; then len (p + q) <= (len q) -' 1 by XREAL_0:def_2; then (p + q) . ((len q) -' 1) = 0. L by ALGSEQ_1:8; hence contradiction by A5, A4, ALGSEQ_1:10; ::_thesis: verum end; ( max ((len p),(len q)) = len q & len (p + q) <= len q ) by A2, Th6, XXREAL_0:def_10; hence len (p + q) = max ((len p),(len q)) by A6, XXREAL_0:1; ::_thesis: verum end; supposeA7: len p > len q ; ::_thesis: len (p + q) = max ((len p),(len q)) then len p >= (len q) + 1 by NAT_1:13; then (len p) - 1 >= len q by XREAL_1:19; then A8: (len p) -' 1 >= len q by XREAL_0:def_2; len p >= 0 + 1 by A7, NAT_1:13; then A9: len p = ((len p) -' 1) + 1 by XREAL_1:235; A10: (p + q) . ((len p) -' 1) = (p . ((len p) -' 1)) + (q . ((len p) -' 1)) by NORMSP_1:def_2 .= (p . ((len p) -' 1)) + (0. L) by A8, ALGSEQ_1:8 .= p . ((len p) -' 1) by RLVECT_1:4 ; A11: len (p + q) >= len p proof assume len (p + q) < len p ; ::_thesis: contradiction then (len (p + q)) + 1 <= len p by NAT_1:13; then len (p + q) <= (len p) - 1 by XREAL_1:19; then len (p + q) <= (len p) -' 1 by XREAL_0:def_2; then (p + q) . ((len p) -' 1) = 0. L by ALGSEQ_1:8; hence contradiction by A10, A9, ALGSEQ_1:10; ::_thesis: verum end; ( max ((len p),(len q)) = len p & len (p + q) <= len p ) by A7, Th6, XXREAL_0:def_10; hence len (p + q) = max ((len p),(len q)) by A11, XXREAL_0:1; ::_thesis: verum end; end; end; theorem Th8: :: POLYNOM4:8 for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of L holds len (- p) = len p proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of L holds len (- p) = len p let p be Polynomial of L; ::_thesis: len (- p) = len p A1: now__::_thesis:_for_n_being_Nat_st_n_is_at_least_length_of_-_p_holds_ len_p_<=_n let n be Nat; ::_thesis: ( n is_at_least_length_of - p implies len p <= n ) assume A2: n is_at_least_length_of - p ; ::_thesis: len p <= n n is_at_least_length_of p proof let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not n <= i or p . i = 0. L ) assume i >= n ; ::_thesis: p . i = 0. L then ( i in NAT & (- p) . i = 0. L ) by A2, ALGSEQ_1:def_2, ORDINAL1:def_12; then - (p . i) = 0. L by BHSP_1:44; hence p . i = 0. L by VECTSP_2:3; ::_thesis: verum end; hence len p <= n by ALGSEQ_1:def_3; ::_thesis: verum end; len p is_at_least_length_of - p proof let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not len p <= i or (- p) . i = 0. L ) assume A3: i >= len p ; ::_thesis: (- p) . i = 0. L i in NAT by ORDINAL1:def_12; hence (- p) . i = - (p . i) by BHSP_1:44 .= - (0. L) by A3, ALGSEQ_1:8 .= 0. L by RLVECT_1:12 ; ::_thesis: verum end; hence len (- p) = len p by A1, ALGSEQ_1:def_3; ::_thesis: verum end; theorem :: POLYNOM4:9 for L being non empty right_complementable add-associative right_zeroed addLoopStr for p, q being Polynomial of L for n being Element of NAT st n >= len p & n >= len q holds n >= len (p - q) proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p, q being Polynomial of L for n being Element of NAT st n >= len p & n >= len q holds n >= len (p - q) let p, q be Polynomial of L; ::_thesis: for n being Element of NAT st n >= len p & n >= len q holds n >= len (p - q) let n be Element of NAT ; ::_thesis: ( n >= len p & n >= len q implies n >= len (p - q) ) assume A1: ( n >= len p & n >= len q ) ; ::_thesis: n >= len (p - q) len q = len (- q) by Th8; hence n >= len (p - q) by A1, Th6; ::_thesis: verum end; theorem :: POLYNOM4:10 for L being non empty right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds len (p *' q) = ((len p) + (len q)) - 1 proof let L be non empty right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds len (p *' q) = ((len p) + (len q)) - 1 let p, q be Polynomial of L; ::_thesis: ( (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L implies len (p *' q) = ((len p) + (len q)) - 1 ) A1: ((len p) + (len q)) -' 1 is_at_least_length_of p *' q proof let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not ((len p) + (len q)) -' 1 <= i or (p *' q) . i = 0. L ) i in NAT by ORDINAL1:def_12; then consider r being FinSequence of the carrier of L such that A2: len r = i + 1 and A3: (p *' q) . i = Sum r and A4: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def_9; assume i >= ((len p) + (len q)) -' 1 ; ::_thesis: (p *' q) . i = 0. L then i >= ((len p) + (len q)) - 1 by XREAL_0:def_2; then i + 1 >= (len p) + (len q) by XREAL_1:20; then len p <= (i + 1) - (len q) by XREAL_1:19; then A5: - (len p) >= - ((i + 1) - (len q)) by XREAL_1:24; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_ r_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom r implies r . b1 = 0. L ) assume A6: k in dom r ; ::_thesis: r . b1 = 0. L then A7: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A4; k in Seg (len r) by A6, FINSEQ_1:def_3; then k <= i + 1 by A2, FINSEQ_1:1; then A8: (i + 1) - k >= 0 by XREAL_1:48; percases ( k -' 1 < len p or k -' 1 >= len p ) ; suppose k -' 1 < len p ; ::_thesis: r . b1 = 0. L then k - 1 < len p by XREAL_0:def_2; then - (k - 1) > - (len p) by XREAL_1:24; then 1 - k > (len q) - (i + 1) by A5, XXREAL_0:2; then (i + 1) + (1 - k) > len q by XREAL_1:19; then ((i + 1) - k) + 1 > len q ; then ((i + 1) -' k) + 1 > len q by A8, XREAL_0:def_2; then (i + 1) -' k >= len q by NAT_1:13; then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8; hence r . k = 0. L by A7, VECTSP_1:6; ::_thesis: verum end; suppose k -' 1 >= len p ; ::_thesis: r . b1 = 0. L then p . (k -' 1) = 0. L by ALGSEQ_1:8; hence r . k = 0. L by A7, VECTSP_1:7; ::_thesis: verum end; end; end; hence (p *' q) . i = 0. L by A3, POLYNOM3:1; ::_thesis: verum end; assume A9: (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L ; ::_thesis: len (p *' q) = ((len p) + (len q)) - 1 A10: now__::_thesis:_not_len_p_<=_0 assume len p <= 0 ; ::_thesis: contradiction then len p = 0 ; then p = 0_. L by Th5; then p . ((len p) -' 1) = 0. L by FUNCOP_1:7; hence contradiction by A9, VECTSP_1:7; ::_thesis: verum end; A11: now__::_thesis:_not_len_q_<=_0 assume len q <= 0 ; ::_thesis: contradiction then len q = 0 ; then q = 0_. L by Th5; then q . ((len q) -' 1) = 0. L by FUNCOP_1:7; hence contradiction by A9, VECTSP_1:6; ::_thesis: verum end; then (len p) + (len q) >= 0 + 1 by NAT_1:13; then A12: ((len p) + (len q)) - 1 >= 1 - 1 by XREAL_1:9; now__::_thesis:_for_n_being_Nat_st_n_is_at_least_length_of_p_*'_q_holds_ not_((len_p)_+_(len_q))_-'_1_>_n let n be Nat; ::_thesis: ( n is_at_least_length_of p *' q implies not ((len p) + (len q)) -' 1 > n ) assume that A13: n is_at_least_length_of p *' q and A14: ((len p) + (len q)) -' 1 > n ; ::_thesis: contradiction ((len p) + (len q)) -' 1 >= n + 1 by A14, NAT_1:13; then A15: (((len p) + (len q)) -' 1) - 1 >= n by XREAL_1:19; A16: (((len p) + (len q)) -' 1) - 1 = (((len p) + (len q)) - 1) - 1 by A12, XREAL_0:def_2; A17: len q >= 0 + 1 by A11, NAT_1:13; then A18: (len q) - 1 >= 0 by XREAL_1:19; (len p) + (len q) > 0 + 1 by A10, A17, XREAL_1:8; then (len p) + (len q) >= 1 + 1 by NAT_1:13; then A19: ((len p) + (len q)) - 2 >= 2 - 2 by XREAL_1:9; then A20: ((len p) + (len q)) -' 2 = ((len p) + (len q)) - (1 + 1) by XREAL_0:def_2; consider r being FinSequence of the carrier of L such that A21: len r = (((len p) + (len q)) -' 2) + 1 and A22: (p *' q) . (((len p) + (len q)) -' 2) = Sum r and A23: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . (((((len p) + (len q)) -' 2) + 1) -' k)) by POLYNOM3:def_9; A24: len r = ((((len p) + (len q)) - 1) + (- 1)) + 1 by A21, A19, XREAL_0:def_2 .= (len p) + ((len q) - 1) ; then A25: ((((len p) + (len q)) -' 2) + 1) -' (len p) = ((((len p) + (len q)) -' 2) + 1) - (len p) by A21, A18, XREAL_0:def_2 .= (len q) -' 1 by A21, A18, A24, XREAL_0:def_2 ; (len r) - (len p) = (len q) - 1 by A24; then A26: (len p) + 0 <= len r by A18, XREAL_1:19; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(r_/^_(len_p))_holds_ (r_/^_(len_p))_._i_=_0._L let i be Element of NAT ; ::_thesis: ( i in dom (r /^ (len p)) implies (r /^ (len p)) . i = 0. L ) assume A27: i in dom (r /^ (len p)) ; ::_thesis: (r /^ (len p)) . i = 0. L then A28: i in Seg (len (r /^ (len p))) by FINSEQ_1:def_3; then A29: 1 <= i by FINSEQ_1:1; i + (len p) >= i by NAT_1:11; then i + (len p) >= 0 + 1 by A29, XXREAL_0:2; then (i + (len p)) - 1 >= 0 by XREAL_1:19; then A30: (i + (len p)) -' 1 = (len p) + (i - 1) by XREAL_0:def_2; 0 + 1 <= i by A28, FINSEQ_1:1; then i - 1 >= 0 by XREAL_1:19; then A31: (i + (len p)) -' 1 >= (len p) + 0 by A30, XREAL_1:6; i <= len (r /^ (len p)) by A28, FINSEQ_1:1; then i <= (len r) - (len p) by A26, RFINSEQ:def_1; then A32: i + (len p) <= len r by XREAL_1:19; i + (len p) >= i by NAT_1:11; then i + (len p) >= 1 by A29, XXREAL_0:2; then i + (len p) in Seg (len r) by A32, FINSEQ_1:1; then A33: i + (len p) in dom r by FINSEQ_1:def_3; thus (r /^ (len p)) . i = r . (i + (len p)) by A26, A27, RFINSEQ:def_1 .= (p . ((i + (len p)) -' 1)) * (q . (((((len p) + (len q)) -' 2) + 1) -' (i + (len p)))) by A23, A33 .= (0. L) * (q . (((((len p) + (len q)) -' 2) + 1) -' (i + (len p)))) by A31, ALGSEQ_1:8 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; then A34: Sum (r /^ (len p)) = 0. L by POLYNOM3:1; A35: len p >= 0 + 1 by A10, NAT_1:13; then len p in Seg (len r) by A26, FINSEQ_1:1; then A36: len p in dom r by FINSEQ_1:def_3; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(r_|_((len_p)_-'_1))_holds_ (r_|_((len_p)_-'_1))_._i_=_0._L A37: (len p) - 1 >= 1 - 1 by A35, XREAL_1:9; A38: (((len p) + (len q)) -' 2) + 1 = ((len p) - 1) + (len q) by A21, A24 .= ((len p) -' 1) + (len q) by A37, XREAL_0:def_2 ; A39: dom (r | ((len p) -' 1)) c= dom r by FINSEQ_5:18; let i be Element of NAT ; ::_thesis: ( i in dom (r | ((len p) -' 1)) implies (r | ((len p) -' 1)) . i = 0. L ) assume A40: i in dom (r | ((len p) -' 1)) ; ::_thesis: (r | ((len p) -' 1)) . i = 0. L len p < (len r) + 1 by A26, NAT_1:13; then (len p) - 1 < ((len r) + 1) - 1 by XREAL_1:9; then (len p) -' 1 < len r by A37, XREAL_0:def_2; then len (r | ((len p) -' 1)) = (len p) -' 1 by FINSEQ_1:59; then i in Seg ((len p) -' 1) by A40, FINSEQ_1:def_3; then i <= (len p) -' 1 by FINSEQ_1:1; then i + (len q) <= ((len p) -' 1) + (len q) by XREAL_1:6; then len q <= ((((len p) + (len q)) -' 2) + 1) - i by A38, XREAL_1:19; then A41: len q <= ((((len p) + (len q)) -' 2) + 1) -' i by XREAL_0:def_2; thus (r | ((len p) -' 1)) . i = (r | ((len p) -' 1)) /. i by A40, PARTFUN1:def_6 .= r /. i by A40, FINSEQ_4:70 .= r . i by A40, A39, PARTFUN1:def_6 .= (p . (i -' 1)) * (q . (((((len p) + (len q)) -' 2) + 1) -' i)) by A23, A40, A39 .= (p . (i -' 1)) * (0. L) by A41, ALGSEQ_1:8 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; then A42: Sum (r | ((len p) -' 1)) = 0. L by POLYNOM3:1; r = ((r | ((len p) -' 1)) ^ <*(r . (len p))*>) ^ (r /^ (len p)) by A26, A35, FINSEQ_5:84; then r = ((r | ((len p) -' 1)) ^ <*(r /. (len p))*>) ^ (r /^ (len p)) by A26, A35, FINSEQ_4:15; then Sum r = (Sum ((r | ((len p) -' 1)) ^ <*(r /. (len p))*>)) + (Sum (r /^ (len p))) by RLVECT_1:41 .= ((Sum (r | ((len p) -' 1))) + (Sum <*(r /. (len p))*>)) + (Sum (r /^ (len p))) by RLVECT_1:41 ; then Sum r = (Sum <*(r /. (len p))*>) + (0. L) by A42, A34, RLVECT_1:4 .= Sum <*(r /. (len p))*> by RLVECT_1:4 .= r /. (len p) by RLVECT_1:44 .= r . (len p) by A36, PARTFUN1:def_6 .= (p . ((len p) -' 1)) * (q . ((len q) -' 1)) by A23, A36, A25 ; hence contradiction by A9, A13, A22, A16, A20, A15, ALGSEQ_1:def_2; ::_thesis: verum end; then len (p *' q) = ((len p) + (len q)) -' 1 by A1, ALGSEQ_1:def_3; hence len (p *' q) = ((len p) + (len q)) - 1 by A12, XREAL_0:def_2; ::_thesis: verum end; begin definition let L be non empty ZeroStr ; let p be Polynomial of L; func Leading-Monomial p -> sequence of L means :Def1: :: POLYNOM4:def 1 ( it . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds it . n = 0. L ) ); existence ex b1 being sequence of L st ( b1 . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds b1 . n = 0. L ) ) proof reconsider P = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) as sequence of L ; take P ; ::_thesis: ( P . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds P . n = 0. L ) ) (len p) -' 1 in NAT ; then (len p) -' 1 in dom (0_. L) by NORMSP_1:12; hence P . ((len p) -' 1) = p . ((len p) -' 1) by FUNCT_7:31; ::_thesis: for n being Element of NAT st n <> (len p) -' 1 holds P . n = 0. L let n be Element of NAT ; ::_thesis: ( n <> (len p) -' 1 implies P . n = 0. L ) assume n <> (len p) -' 1 ; ::_thesis: P . n = 0. L hence P . n = (0_. L) . n by FUNCT_7:32 .= 0. L by FUNCOP_1:7 ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of L st b1 . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds b1 . n = 0. L ) & b2 . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds b2 . n = 0. L ) holds b1 = b2 proof let P1, P2 be sequence of L; ::_thesis: ( P1 . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds P1 . n = 0. L ) & P2 . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds P2 . n = 0. L ) implies P1 = P2 ) assume that A1: P1 . ((len p) -' 1) = p . ((len p) -' 1) and A2: for n being Element of NAT st n <> (len p) -' 1 holds P1 . n = 0. L and A3: P2 . ((len p) -' 1) = p . ((len p) -' 1) and A4: for n being Element of NAT st n <> (len p) -' 1 holds P2 . n = 0. L ; ::_thesis: P1 = P2 now__::_thesis:_for_i_being_Element_of_NAT_holds_P1_._i_=_P2_._i let i be Element of NAT ; ::_thesis: P1 . b1 = P2 . b1 percases ( i = (len p) -' 1 or i <> (len p) -' 1 ) ; suppose i = (len p) -' 1 ; ::_thesis: P1 . b1 = P2 . b1 hence P1 . i = P2 . i by A1, A3; ::_thesis: verum end; supposeA5: i <> (len p) -' 1 ; ::_thesis: P1 . b1 = P2 . b1 hence P1 . i = 0. L by A2 .= P2 . i by A4, A5 ; ::_thesis: verum end; end; end; hence P1 = P2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines Leading-Monomial POLYNOM4:def_1_:_ for L being non empty ZeroStr for p being Polynomial of L for b3 being sequence of L holds ( b3 = Leading-Monomial p iff ( b3 . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds b3 . n = 0. L ) ) ); theorem Th11: :: POLYNOM4:11 for L being non empty ZeroStr for p being Polynomial of L holds Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L holds Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) let p be Polynomial of L; ::_thesis: Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) reconsider P = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) as sequence of L ; A1: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<>_(len_p)_-'_1_holds_ P_._n_=_0._L let n be Element of NAT ; ::_thesis: ( n <> (len p) -' 1 implies P . n = 0. L ) assume n <> (len p) -' 1 ; ::_thesis: P . n = 0. L hence P . n = (0_. L) . n by FUNCT_7:32 .= 0. L by FUNCOP_1:7 ; ::_thesis: verum end; (len p) -' 1 in NAT ; then (len p) -' 1 in dom (0_. L) by NORMSP_1:12; then P . ((len p) -' 1) = p . ((len p) -' 1) by FUNCT_7:31; hence Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) by A1, Def1; ::_thesis: verum end; registration let L be non empty ZeroStr ; let p be Polynomial of L; cluster Leading-Monomial p -> finite-Support ; coherence Leading-Monomial p is finite-Support proof take len p ; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds ( not len p <= b1 or (Leading-Monomial p) . b1 = 0. L ) let i be Nat; ::_thesis: ( not len p <= i or (Leading-Monomial p) . i = 0. L ) A1: i in NAT by ORDINAL1:def_12; assume i >= len p ; ::_thesis: (Leading-Monomial p) . i = 0. L then i + 1 > len p by NAT_1:13; then A2: (i + 1) - 1 > (len p) - 1 by XREAL_1:9; A3: Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) by Th11; percases ( len p > 0 or len p = 0 ) ; suppose len p > 0 ; ::_thesis: (Leading-Monomial p) . i = 0. L then len p >= 0 + 1 by NAT_1:13; then (len p) - 1 >= (0 + 1) - 1 by XREAL_1:9; then i <> (len p) -' 1 by A2, XREAL_0:def_2; hence (Leading-Monomial p) . i = (0_. L) . i by A3, FUNCT_7:32 .= 0. L by A1, FUNCOP_1:7 ; ::_thesis: verum end; supposeA4: len p = 0 ; ::_thesis: (Leading-Monomial p) . i = 0. L then A5: (len p) -' 1 = 0 by NAT_2:8; 0 in NAT ; then A6: 0 in dom (0_. L) by NORMSP_1:12; now__::_thesis:_(Leading-Monomial_p)_._i_=_0._L percases ( i > 0 or i = 0 ) ; suppose i > 0 ; ::_thesis: (Leading-Monomial p) . i = 0. L hence (Leading-Monomial p) . i = (0_. L) . i by A3, A5, FUNCT_7:32 .= 0. L by A1, FUNCOP_1:7 ; ::_thesis: verum end; suppose i = 0 ; ::_thesis: (Leading-Monomial p) . i = 0. L hence (Leading-Monomial p) . i = p . 0 by A3, A5, A6, FUNCT_7:31 .= (0_. L) . 0 by A4, Th5 .= 0. L by FUNCOP_1:7 ; ::_thesis: verum end; end; end; hence (Leading-Monomial p) . i = 0. L ; ::_thesis: verum end; end; end; end; theorem Th12: :: POLYNOM4:12 for L being non empty ZeroStr for p being Polynomial of L st len p = 0 holds Leading-Monomial p = 0_. L proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L st len p = 0 holds Leading-Monomial p = 0_. L let p be Polynomial of L; ::_thesis: ( len p = 0 implies Leading-Monomial p = 0_. L ) assume len p = 0 ; ::_thesis: Leading-Monomial p = 0_. L then A1: (0_. L) . ((len p) -' 1) = p . ((len p) -' 1) by Th5; for n being Element of NAT st n <> (len p) -' 1 holds (0_. L) . n = 0. L by FUNCOP_1:7; hence Leading-Monomial p = 0_. L by A1, Def1; ::_thesis: verum end; theorem :: POLYNOM4:13 for L being non empty ZeroStr holds Leading-Monomial (0_. L) = 0_. L proof let L be non empty ZeroStr ; ::_thesis: Leading-Monomial (0_. L) = 0_. L len (0_. L) = 0 by Th3; hence Leading-Monomial (0_. L) = 0_. L by Th12; ::_thesis: verum end; theorem :: POLYNOM4:14 for L being non empty non degenerated multLoopStr_0 holds Leading-Monomial (1_. L) = 1_. L proof let L be non empty non degenerated multLoopStr_0 ; ::_thesis: Leading-Monomial (1_. L) = 1_. L A1: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<>_(len_(1_._L))_-'_1_holds_ (1_._L)_._n_=_0._L let n be Element of NAT ; ::_thesis: ( n <> (len (1_. L)) -' 1 implies (1_. L) . n = 0. L ) assume n <> (len (1_. L)) -' 1 ; ::_thesis: (1_. L) . n = 0. L then n <> 1 -' 1 by Th4; then n <> 0 by XREAL_1:232; hence (1_. L) . n = 0. L by POLYNOM3:30; ::_thesis: verum end; (1_. L) . ((len (1_. L)) -' 1) = (1_. L) . ((len (1_. L)) -' 1) ; hence Leading-Monomial (1_. L) = 1_. L by A1, Def1; ::_thesis: verum end; theorem Th15: :: POLYNOM4:15 for L being non empty ZeroStr for p being Polynomial of L holds len (Leading-Monomial p) = len p proof let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L holds len (Leading-Monomial p) = len p let p be Polynomial of L; ::_thesis: len (Leading-Monomial p) = len p set r = Leading-Monomial p; A1: Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) by Th11; percases ( len p > 0 or len p = 0 ) ; suppose len p > 0 ; ::_thesis: len (Leading-Monomial p) = len p then A2: len p >= 0 + 1 by NAT_1:13; (len p) -' 1 in NAT ; then A3: (len p) -' 1 in dom (0_. L) by NORMSP_1:12; A4: now__::_thesis:_for_m_being_Nat_st_m_is_at_least_length_of_Leading-Monomial_p_holds_ not_len_p_>_m let m be Nat; ::_thesis: ( m is_at_least_length_of Leading-Monomial p implies not len p > m ) assume A5: m is_at_least_length_of Leading-Monomial p ; ::_thesis: not len p > m assume len p > m ; ::_thesis: contradiction then len p >= m + 1 by NAT_1:13; then (len p) - 1 >= (m + 1) - 1 by XREAL_1:9; then (len p) -' 1 >= m by XREAL_0:def_2; then (Leading-Monomial p) . ((len p) -' 1) = 0. L by A5, ALGSEQ_1:def_2; then A6: p . ((len p) -' 1) = 0. L by A1, A3, FUNCT_7:31; len p = ((len p) -' 1) + 1 by A2, XREAL_1:235; hence contradiction by A6, ALGSEQ_1:10; ::_thesis: verum end; A7: (len p) - 1 >= 0 by A2, XREAL_1:19; len p is_at_least_length_of Leading-Monomial p proof let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not len p <= i or (Leading-Monomial p) . i = 0. L ) A8: i in NAT by ORDINAL1:def_12; assume i >= len p ; ::_thesis: (Leading-Monomial p) . i = 0. L then i + 1 > len p by NAT_1:13; then (i + 1) - 1 > (len p) - 1 by XREAL_1:9; then i <> (len p) -' 1 by A7, XREAL_0:def_2; hence (Leading-Monomial p) . i = (0_. L) . i by A1, FUNCT_7:32 .= 0. L by A8, FUNCOP_1:7 ; ::_thesis: verum end; hence len (Leading-Monomial p) = len p by A4, ALGSEQ_1:def_3; ::_thesis: verum end; supposeA9: len p = 0 ; ::_thesis: len (Leading-Monomial p) = len p hence len (Leading-Monomial p) = len (0_. L) by Th12 .= len p by A9, Th5 ; ::_thesis: verum end; end; end; theorem Th16: :: POLYNOM4:16 for L being non empty right_complementable add-associative right_zeroed addLoopStr for p being Polynomial of L st len p <> 0 holds ex q being Polynomial of L st ( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds q . n = p . n ) ) proof let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Polynomial of L st len p <> 0 holds ex q being Polynomial of L st ( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds q . n = p . n ) ) let p be Polynomial of L; ::_thesis: ( len p <> 0 implies ex q being Polynomial of L st ( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds q . n = p . n ) ) ) deffunc H1( Element of NAT ) -> Element of the carrier of L = p . $1; consider q being Polynomial of L such that A1: len q <= (len p) -' 1 and A2: for n being Element of NAT st n < (len p) -' 1 holds q . n = H1(n) from POLYNOM3:sch_2(); assume len p <> 0 ; ::_thesis: ex q being Polynomial of L st ( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds q . n = p . n ) ) then A3: len p >= 0 + 1 by NAT_1:13; take q ; ::_thesis: ( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds q . n = p . n ) ) len q < ((len p) -' 1) + 1 by A1, NAT_1:13; hence A4: len q < len p by A3, XREAL_1:235; ::_thesis: ( p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds q . n = p . n ) ) A5: now__::_thesis:_for_k_being_Nat_st_k_<_len_p_holds_ (q_+_(Leading-Monomial_p))_._k_=_p_._k let k be Nat; ::_thesis: ( k < len p implies (q + (Leading-Monomial p)) . b1 = p . b1 ) A6: k in NAT by ORDINAL1:def_12; assume k < len p ; ::_thesis: (q + (Leading-Monomial p)) . b1 = p . b1 then k + 1 <= len p by NAT_1:13; then A7: (k + 1) - 1 <= (len p) - 1 by XREAL_1:9; percases ( k < (len p) - 1 or k = (len p) - 1 ) by A7, XXREAL_0:1; suppose k < (len p) - 1 ; ::_thesis: (q + (Leading-Monomial p)) . b1 = p . b1 then A8: k < (len p) -' 1 by XREAL_0:def_2; thus (q + (Leading-Monomial p)) . k = (q . k) + ((Leading-Monomial p) . k) by A6, NORMSP_1:def_2 .= (p . k) + ((Leading-Monomial p) . k) by A2, A6, A8 .= (p . k) + (0. L) by A6, A8, Def1 .= p . k by RLVECT_1:def_4 ; ::_thesis: verum end; suppose k = (len p) - 1 ; ::_thesis: (q + (Leading-Monomial p)) . b1 = p . b1 then A9: k = (len p) -' 1 by XREAL_0:def_2; hence (q + (Leading-Monomial p)) . k = (q . k) + ((Leading-Monomial p) . k) by NORMSP_1:def_2 .= (0. L) + ((Leading-Monomial p) . k) by A1, A9, ALGSEQ_1:8 .= (Leading-Monomial p) . k by RLVECT_1:4 .= p . k by A9, Def1 ; ::_thesis: verum end; end; end; A10: len (Leading-Monomial p) = len p by Th15; then len (q + (Leading-Monomial p)) = max ((len q),(len (Leading-Monomial p))) by A4, Th7 .= len p by A4, A10, XXREAL_0:def_10 ; hence p = q + (Leading-Monomial p) by A5, ALGSEQ_1:12; ::_thesis: for n being Element of NAT st n < (len p) - 1 holds q . n = p . n let n be Element of NAT ; ::_thesis: ( n < (len p) - 1 implies q . n = p . n ) assume n < (len p) - 1 ; ::_thesis: q . n = p . n then n < (len p) -' 1 by XREAL_0:def_2; hence q . n = p . n by A2; ::_thesis: verum end; begin definition let L be non empty unital doubleLoopStr ; let p be Polynomial of L; let x be Element of L; func eval (p,x) -> Element of L means :Def2: :: POLYNOM4:def 2 ex F being FinSequence of the carrier of L st ( it = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ); existence ex b1 being Element of L ex F being FinSequence of the carrier of L st ( b1 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) proof deffunc H1( Nat) -> Element of the carrier of L = (p . ($1 -' 1)) * ((power L) . (x,($1 -' 1))); consider F being FinSequence of the carrier of L such that A1: len F = len p and A2: for n being Nat st n in dom F holds F . n = H1(n) from FINSEQ_2:sch_1(); take y = Sum F; ::_thesis: ex F being FinSequence of the carrier of L st ( y = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) take F ; ::_thesis: ( y = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) thus ( y = Sum F & len F = len p ) by A1; ::_thesis: for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) let n be Element of NAT ; ::_thesis: ( n in dom F implies F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) assume n in dom F ; ::_thesis: F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) hence F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Element of L st ex F being FinSequence of the carrier of L st ( b1 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) & ex F being FinSequence of the carrier of L st ( b2 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) holds b1 = b2 proof let y1, y2 be Element of L; ::_thesis: ( ex F being FinSequence of the carrier of L st ( y1 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) & ex F being FinSequence of the carrier of L st ( y2 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) implies y1 = y2 ) given F1 being FinSequence of the carrier of L such that A3: y1 = Sum F1 and A4: len F1 = len p and A5: for n being Element of NAT st n in dom F1 holds F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ; ::_thesis: ( for F being FinSequence of the carrier of L holds ( not y2 = Sum F or not len F = len p or ex n being Element of NAT st ( n in dom F & not F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) or y1 = y2 ) given F2 being FinSequence of the carrier of L such that A6: y2 = Sum F2 and A7: len F2 = len p and A8: for n being Element of NAT st n in dom F2 holds F2 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ; ::_thesis: y1 = y2 A9: dom F1 = Seg (len p) by A4, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_F1_holds_ F1_._n_=_F2_._n let n be Nat; ::_thesis: ( n in dom F1 implies F1 . n = F2 . n ) assume A10: n in dom F1 ; ::_thesis: F1 . n = F2 . n then A11: n in dom F2 by A7, A9, FINSEQ_1:def_3; thus F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by A5, A10 .= F2 . n by A8, A11 ; ::_thesis: verum end; hence y1 = y2 by A3, A4, A6, A7, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def2 defines eval POLYNOM4:def_2_:_ for L being non empty unital doubleLoopStr for p being Polynomial of L for x, b4 being Element of L holds ( b4 = eval (p,x) iff ex F being FinSequence of the carrier of L st ( b4 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) ); theorem Th17: :: POLYNOM4:17 for L being non empty unital doubleLoopStr for x being Element of L holds eval ((0_. L),x) = 0. L proof let L be non empty unital doubleLoopStr ; ::_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 consider F being FinSequence of the carrier of L such that A1: eval ((0_. L),x) = Sum F and A2: len F = len (0_. L) and for n being Element of NAT st n in dom F holds F . n = ((0_. L) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; len F = 0 by A2, Th3; then F = <*> the carrier of L ; hence eval ((0_. L),x) = 0. L by A1, RLVECT_1:43; ::_thesis: verum end; theorem Th18: :: POLYNOM4:18 for L being non empty non degenerated right_complementable add-associative right_zeroed associative well-unital doubleLoopStr for x being Element of L holds eval ((1_. L),x) = 1. L proof let L be non empty non degenerated right_complementable add-associative right_zeroed associative well-unital doubleLoopStr ; ::_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 consider F being FinSequence of the carrier of L such that A1: eval ((1_. L),x) = Sum F and A2: len F = len (1_. L) and A3: for n being Element of NAT st n in dom F holds F . n = ((1_. L) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; A4: len F = 1 by A2, Th4; then 1 in Seg (len F) by FINSEQ_1:1; then 1 in dom F by FINSEQ_1:def_3; then F . 1 = ((1_. L) . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A3 .= ((1_. L) . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232 .= (1. L) * ((power L) . (x,(1 -' 1))) by POLYNOM3:30 .= (power L) . (x,(1 -' 1)) by VECTSP_1:def_8 .= (power L) . (x,0) by XREAL_1:232 .= 1_ L by GROUP_1:def_7 .= 1. L ; then F = <*(1. L)*> by A4, FINSEQ_1:40; hence eval ((1_. L),x) = 1. L by A1, RLVECT_1:44; ::_thesis: verum end; Lm2: for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr for x being Element of F holds (0. F) * x = 0. F proof let F be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for x being Element of F holds (0. F) * x = 0. F let x be Element of F; ::_thesis: (0. F) * x = 0. F ((0. F) * x) + (0. F) = (((0. F) + (0. F)) * x) + (0. F) by RLVECT_1:4 .= ((0. F) + (0. F)) * x by RLVECT_1:4 .= ((0. F) * x) + ((0. F) * x) by VECTSP_1:def_3 ; hence (0. F) * x = 0. F by RLVECT_1:8; ::_thesis: verum end; theorem Th19: :: POLYNOM4:19 for L being non empty right_complementable Abelian add-associative right_zeroed unital left-distributive doubleLoopStr for p, q being Polynomial of L for x being Element of L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) proof let L be non empty right_complementable Abelian add-associative right_zeroed unital left-distributive doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for x being Element of L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) let p, q be Polynomial of L; ::_thesis: for x being Element of L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) let x be Element of L; ::_thesis: eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) reconsider k = max ((len p),(len q)) as Element of NAT by FINSEQ_2:1; A1: k - (len p) >= 0 by XREAL_1:48, XXREAL_0:25; consider F1 being FinSequence of the carrier of L such that A2: eval (p,x) = Sum F1 and A3: len F1 = len p and A4: for n being Element of NAT st n in dom F1 holds F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; A5: len (F1 ^ ((k -' (len F1)) |-> (0. L))) = (len p) + (len ((k -' (len p)) |-> (0. L))) by A3, FINSEQ_1:22 .= (len p) + (k -' (len p)) by CARD_1:def_7 .= (len p) + (k - (len p)) by A1, XREAL_0:def_2 .= k ; A6: k - (len q) >= 0 by XREAL_1:48, XXREAL_0:25; ( k >= len p & k >= len q ) by XXREAL_0:25; then A7: k - (len (p + q)) >= 0 by Th6, XREAL_1:48; consider F3 being FinSequence of the carrier of L such that A8: eval ((p + q),x) = Sum F3 and A9: len F3 = len (p + q) and A10: for n being Element of NAT st n in dom F3 holds F3 . n = ((p + q) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; A11: len (F3 ^ ((k -' (len F3)) |-> (0. L))) = (len (p + q)) + (len ((k -' (len (p + q))) |-> (0. L))) by A9, FINSEQ_1:22 .= (len (p + q)) + (k -' (len (p + q))) by CARD_1:def_7 .= (len (p + q)) + (k - (len (p + q))) by A7, XREAL_0:def_2 .= k ; consider F2 being FinSequence of the carrier of L such that A12: eval (q,x) = Sum F2 and A13: len F2 = len q and A14: for n being Element of NAT st n in dom F2 holds F2 . n = (q . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; len (F2 ^ ((k -' (len F2)) |-> (0. L))) = (len q) + (len ((k -' (len q)) |-> (0. L))) by A13, FINSEQ_1:22 .= (len q) + (k -' (len q)) by CARD_1:def_7 .= (len q) + (k - (len q)) by A6, XREAL_0:def_2 .= k ; then reconsider G1 = F1 ^ ((k -' (len F1)) |-> (0. L)), G2 = F2 ^ ((k -' (len F2)) |-> (0. L)), G3 = F3 ^ ((k -' (len F3)) |-> (0. L)) as Element of k -tuples_on the carrier of L by A5, A11, FINSEQ_2:92; now__::_thesis:_for_n_being_Nat_st_n_in_Seg_k_holds_ G3_._n_=_(G1_+_G2)_._n let n be Nat; ::_thesis: ( n in Seg k implies G3 . b1 = (G1 + G2) . b1 ) assume A15: n in Seg k ; ::_thesis: G3 . b1 = (G1 + G2) . b1 then A16: 0 + 1 <= n by FINSEQ_1:1; A17: n <= k by A15, FINSEQ_1:1; percases ( len p > len q or len p < len q or len p = len q ) by XXREAL_0:1; supposeA18: len p > len q ; ::_thesis: G3 . b1 = (G1 + G2) . b1 then A19: k = len p by XXREAL_0:def_10; then len (p + q) = len p by A18, Th7; then A20: n in dom F3 by A9, A15, A19, FINSEQ_1:def_3; A21: len G2 = k by CARD_1:def_7; then A22: n in dom G2 by A15, FINSEQ_1:def_3; then A23: G2 /. n = G2 . n by PARTFUN1:def_6; len G1 = k by CARD_1:def_7; then A24: n in dom G1 by A15, FINSEQ_1:def_3; then A25: G1 /. n = G1 . n by PARTFUN1:def_6; A26: n in dom F1 by A3, A15, A19, FINSEQ_1:def_3; A27: G1 /. n = G1 . n by A24, PARTFUN1:def_6 .= F1 . n by A26, FINSEQ_1:def_7 .= F1 /. n by A26, PARTFUN1:def_6 ; A28: F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by A4, A26; now__::_thesis:_G3_._n_=_(G1_+_G2)_._n percases ( n <= len q or n > len q ) ; suppose n <= len q ; ::_thesis: G3 . n = (G1 + G2) . n then n in Seg (len q) by A16, FINSEQ_1:1; then A29: n in dom F2 by A13, FINSEQ_1:def_3; then A30: F2 . n = (q . (n -' 1)) * ((power L) . (x,(n -' 1))) by A14; A31: G2 /. n = G2 . n by A22, PARTFUN1:def_6 .= F2 . n by A29, FINSEQ_1:def_7 .= F2 /. n by A29, PARTFUN1:def_6 ; thus G3 . n = F3 . n by A20, FINSEQ_1:def_7 .= ((p + q) . (n -' 1)) * ((power L) . (x,(n -' 1))) by A10, A20 .= ((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . (x,(n -' 1))) by NORMSP_1:def_2 .= ((p . (n -' 1)) * ((power L) . (x,(n -' 1)))) + ((q . (n -' 1)) * ((power L) . (x,(n -' 1)))) by VECTSP_1:def_3 .= ((p . (n -' 1)) * ((power L) . (x,(n -' 1)))) + (F2 /. n) by A29, A30, PARTFUN1:def_6 .= (F1 /. n) + (F2 /. n) by A26, A28, PARTFUN1:def_6 .= (G1 + G2) . n by A15, A25, A23, A27, A31, FVSUM_1:18 ; ::_thesis: verum end; supposeA32: n > len q ; ::_thesis: G3 . n = (G1 + G2) . n then A33: n >= (len q) + 1 by NAT_1:13; then n - 1 >= len q by XREAL_1:19; then A34: n -' 1 >= len q by XREAL_0:def_2; n - (len F2) <= k - (len F2) by A17, XREAL_1:9; then A35: n - (len F2) <= k -' (len F2) by XREAL_0:def_2; A36: n - (len F2) >= 1 by A13, A33, XREAL_1:19; then n - (len F2) = n -' (len F2) by XREAL_0:def_2; then A37: n - (len F2) in Seg (k -' (len F2)) by A36, A35, FINSEQ_1:1; n <= len G2 by A15, A21, FINSEQ_1:1; then A38: G2 /. n = ((k -' (len F2)) |-> (0. L)) . (n - (len F2)) by A13, A23, A32, FINSEQ_1:24 .= 0. L by A37, FUNCOP_1:7 ; thus G3 . n = F3 . n by A20, FINSEQ_1:def_7 .= ((p + q) . (n -' 1)) * ((power L) . (x,(n -' 1))) by A10, A20 .= ((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . (x,(n -' 1))) by NORMSP_1:def_2 .= ((p . (n -' 1)) + (0. L)) * ((power L) . (x,(n -' 1))) by A34, ALGSEQ_1:8 .= (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by RLVECT_1:4 .= F1 . n by A4, A26 .= G1 /. n by A26, A27, PARTFUN1:def_6 .= (G1 /. n) + (0. L) by RLVECT_1:4 .= (G1 + G2) . n by A15, A25, A23, A38, FVSUM_1:18 ; ::_thesis: verum end; end; end; hence G3 . n = (G1 + G2) . n ; ::_thesis: verum end; supposeA39: len p < len q ; ::_thesis: G3 . b1 = (G1 + G2) . b1 then A40: k = len q by XXREAL_0:def_10; then len (p + q) = len q by A39, Th7; then A41: n in dom F3 by A9, A15, A40, FINSEQ_1:def_3; A42: len G1 = k by CARD_1:def_7; then A43: n in dom G1 by A15, FINSEQ_1:def_3; then A44: G1 /. n = G1 . n by PARTFUN1:def_6; len G2 = k by CARD_1:def_7; then A45: n in dom G2 by A15, FINSEQ_1:def_3; then A46: G2 /. n = G2 . n by PARTFUN1:def_6; A47: n in dom F2 by A13, A15, A40, FINSEQ_1:def_3; A48: G2 /. n = G2 . n by A45, PARTFUN1:def_6 .= F2 . n by A47, FINSEQ_1:def_7 .= F2 /. n by A47, PARTFUN1:def_6 ; A49: F2 . n = (q . (n -' 1)) * ((power L) . (x,(n -' 1))) by A14, A47; now__::_thesis:_G3_._n_=_(G1_+_G2)_._n percases ( n <= len p or n > len p ) ; suppose n <= len p ; ::_thesis: G3 . n = (G1 + G2) . n then n in Seg (len p) by A16, FINSEQ_1:1; then A50: n in dom F1 by A3, FINSEQ_1:def_3; then A51: F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by A4; A52: G1 /. n = G1 . n by A43, PARTFUN1:def_6 .= F1 . n by A50, FINSEQ_1:def_7 .= F1 /. n by A50, PARTFUN1:def_6 ; thus G3 . n = F3 . n by A41, FINSEQ_1:def_7 .= ((p + q) . (n -' 1)) * ((power L) . (x,(n -' 1))) by A10, A41 .= ((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . (x,(n -' 1))) by NORMSP_1:def_2 .= ((p . (n -' 1)) * ((power L) . (x,(n -' 1)))) + ((q . (n -' 1)) * ((power L) . (x,(n -' 1)))) by VECTSP_1:def_3 .= (F1 /. n) + ((q . (n -' 1)) * ((power L) . (x,(n -' 1)))) by A50, A51, PARTFUN1:def_6 .= (F1 /. n) + (F2 /. n) by A47, A49, PARTFUN1:def_6 .= (G1 + G2) . n by A15, A44, A46, A48, A52, FVSUM_1:18 ; ::_thesis: verum end; supposeA53: n > len p ; ::_thesis: G3 . n = (G1 + G2) . n then A54: n >= (len p) + 1 by NAT_1:13; then n - 1 >= len p by XREAL_1:19; then A55: n -' 1 >= len p by XREAL_0:def_2; n - (len F1) <= k - (len F1) by A17, XREAL_1:9; then A56: n - (len F1) <= k -' (len F1) by XREAL_0:def_2; A57: n - (len F1) >= 1 by A3, A54, XREAL_1:19; then n - (len F1) = n -' (len F1) by XREAL_0:def_2; then A58: n - (len F1) in Seg (k -' (len F1)) by A57, A56, FINSEQ_1:1; n <= len G1 by A15, A42, FINSEQ_1:1; then A59: G1 /. n = ((k -' (len F1)) |-> (0. L)) . (n - (len F1)) by A3, A44, A53, FINSEQ_1:24 .= 0. L by A58, FUNCOP_1:7 ; thus G3 . n = F3 . n by A41, FINSEQ_1:def_7 .= ((p + q) . (n -' 1)) * ((power L) . (x,(n -' 1))) by A10, A41 .= ((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . (x,(n -' 1))) by NORMSP_1:def_2 .= ((0. L) + (q . (n -' 1))) * ((power L) . (x,(n -' 1))) by A55, ALGSEQ_1:8 .= (q . (n -' 1)) * ((power L) . (x,(n -' 1))) by RLVECT_1:4 .= F2 . n by A14, A47 .= G2 /. n by A47, A48, PARTFUN1:def_6 .= (0. L) + (G2 /. n) by RLVECT_1:4 .= (G1 + G2) . n by A15, A44, A46, A59, FVSUM_1:18 ; ::_thesis: verum end; end; end; hence G3 . n = (G1 + G2) . n ; ::_thesis: verum end; supposeA60: len p = len q ; ::_thesis: G3 . b1 = (G1 + G2) . b1 len G2 = k by CARD_1:def_7; then A61: n in dom G2 by A15, FINSEQ_1:def_3; then A62: G2 /. n = G2 . n by PARTFUN1:def_6; len G1 = k by CARD_1:def_7; then A63: n in dom G1 by A15, FINSEQ_1:def_3; then A64: G1 /. n = G1 . n by PARTFUN1:def_6; A65: len G3 = k by CARD_1:def_7; A66: n in dom F2 by A13, A15, A60, FINSEQ_1:def_3; A67: n in dom F1 by A3, A15, A60, FINSEQ_1:def_3; then A68: F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by A4; A69: G1 /. n = G1 . n by A63, PARTFUN1:def_6 .= F1 . n by A67, FINSEQ_1:def_7 .= F1 /. n by A67, PARTFUN1:def_6 ; now__::_thesis:_G3_._n_=_(G1_+_G2)_._n percases ( n <= len (p + q) or n > len (p + q) ) ; supposeA70: n <= len (p + q) ; ::_thesis: G3 . n = (G1 + G2) . n A71: n in dom F2 by A13, A15, A60, FINSEQ_1:def_3; then A72: F2 . n = (q . (n -' 1)) * ((power L) . (x,(n -' 1))) by A14; A73: G2 /. n = G2 . n by A61, PARTFUN1:def_6 .= F2 . n by A71, FINSEQ_1:def_7 .= F2 /. n by A71, PARTFUN1:def_6 ; n in Seg (len (p + q)) by A16, A70, FINSEQ_1:1; then A74: n in dom F3 by A9, FINSEQ_1:def_3; hence G3 . n = F3 . n by FINSEQ_1:def_7 .= ((p + q) . (n -' 1)) * ((power L) . (x,(n -' 1))) by A10, A74 .= ((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . (x,(n -' 1))) by NORMSP_1:def_2 .= ((p . (n -' 1)) * ((power L) . (x,(n -' 1)))) + ((q . (n -' 1)) * ((power L) . (x,(n -' 1)))) by VECTSP_1:def_3 .= ((p . (n -' 1)) * ((power L) . (x,(n -' 1)))) + (F2 /. n) by A71, A72, PARTFUN1:def_6 .= (F1 /. n) + (F2 /. n) by A67, A68, PARTFUN1:def_6 .= (G1 + G2) . n by A15, A64, A62, A69, A73, FVSUM_1:18 ; ::_thesis: verum end; supposeA75: n > len (p + q) ; ::_thesis: G3 . n = (G1 + G2) . n then A76: n >= (len (p + q)) + 1 by NAT_1:13; then n - 1 >= ((len (p + q)) + 1) - 1 by XREAL_1:9; then A77: n -' 1 >= len (p + q) by XREAL_0:def_2; n - (len F3) <= k - (len F3) by A17, XREAL_1:9; then A78: n - (len F3) <= k -' (len F3) by XREAL_0:def_2; A79: G2 . n = F2 . n by A66, FINSEQ_1:def_7 .= (q . (n -' 1)) * ((power L) . (x,(n -' 1))) by A14, A66 ; A80: G1 . n = F1 . n by A67, FINSEQ_1:def_7 .= (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by A4, A67 ; A81: n - (len F3) >= 1 by A9, A76, XREAL_1:19; then n - (len F3) = n -' (len F3) by XREAL_0:def_2; then A82: n - (len F3) in Seg (k -' (len F3)) by A81, A78, FINSEQ_1:1; n <= len G3 by A15, A65, FINSEQ_1:1; hence G3 . n = ((k -' (len F3)) |-> (0. L)) . (n - (len F3)) by A9, A75, FINSEQ_1:24 .= 0. L by A82, FUNCOP_1:7 .= (0. L) * ((power L) . (x,(n -' 1))) by Lm2 .= ((p + q) . (n -' 1)) * ((power L) . (x,(n -' 1))) by A77, ALGSEQ_1:8 .= ((p . (n -' 1)) + (q . (n -' 1))) * ((power L) . (x,(n -' 1))) by NORMSP_1:def_2 .= ((p . (n -' 1)) * ((power L) . (x,(n -' 1)))) + ((q . (n -' 1)) * ((power L) . (x,(n -' 1)))) by VECTSP_1:def_3 .= (G1 + G2) . n by A15, A80, A79, FVSUM_1:18 ; ::_thesis: verum end; end; end; hence G3 . n = (G1 + G2) . n ; ::_thesis: verum end; end; end; then A83: G3 = G1 + G2 by FINSEQ_2:119; A84: Sum G3 = (Sum F3) + (Sum ((k -' (len F3)) |-> (0. L))) by RLVECT_1:41 .= (Sum F3) + (0. L) by MATRIX_3:11 .= Sum F3 by RLVECT_1:def_4 ; A85: Sum G2 = (Sum F2) + (Sum ((k -' (len F2)) |-> (0. L))) by RLVECT_1:41 .= (Sum F2) + (0. L) by MATRIX_3:11 .= Sum F2 by RLVECT_1:def_4 ; Sum G1 = (Sum F1) + (Sum ((k -' (len F1)) |-> (0. L))) by RLVECT_1:41 .= (Sum F1) + (0. L) by MATRIX_3:11 .= Sum F1 by RLVECT_1:def_4 ; hence eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) by A2, A12, A8, A85, A84, A83, FVSUM_1:76; ::_thesis: verum end; theorem Th20: :: POLYNOM4:20 for L being non empty right_complementable Abelian add-associative right_zeroed unital distributive doubleLoopStr for p being Polynomial of L for x being Element of L holds eval ((- p),x) = - (eval (p,x)) proof let L be non empty right_complementable Abelian add-associative right_zeroed unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L for x being Element of L holds eval ((- p),x) = - (eval (p,x)) let p be Polynomial of L; ::_thesis: for x being Element of L holds eval ((- p),x) = - (eval (p,x)) let x be Element of L; ::_thesis: eval ((- p),x) = - (eval (p,x)) consider F1 being FinSequence of the carrier of L such that A1: eval (p,x) = Sum F1 and A2: len F1 = len p and A3: for n being Element of NAT st n in dom F1 holds F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; consider F2 being FinSequence of the carrier of L such that A4: eval ((- p),x) = Sum F2 and A5: len F2 = len (- p) and A6: for n being Element of NAT st n in dom F2 holds F2 . n = ((- p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; len F2 = len F1 by A2, A5, Th8; then A7: dom F2 = dom F1 by FINSEQ_3:29; now__::_thesis:_for_n_being_Element_of_NAT_ for_v_being_Element_of_L_st_n_in_dom_F2_&_v_=_F1_._n_holds_ F2_._n_=_-_v let n be Element of NAT ; ::_thesis: for v being Element of L st n in dom F2 & v = F1 . n holds F2 . n = - v let v be Element of L; ::_thesis: ( n in dom F2 & v = F1 . n implies F2 . n = - v ) assume that A8: n in dom F2 and A9: v = F1 . n ; ::_thesis: F2 . n = - v thus F2 . n = ((- p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by A6, A8 .= (- (p . (n -' 1))) * ((power L) . (x,(n -' 1))) by BHSP_1:44 .= - ((p . (n -' 1)) * ((power L) . (x,(n -' 1)))) by VECTSP_1:9 .= - v by A3, A7, A8, A9 ; ::_thesis: verum end; hence eval ((- p),x) = - (eval (p,x)) by A1, A2, A4, A5, Th8, RLVECT_1:40; ::_thesis: verum end; theorem :: POLYNOM4:21 for L being non empty right_complementable Abelian add-associative right_zeroed unital distributive doubleLoopStr for p, q being Polynomial of L for x being Element of L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x)) proof let L be non empty right_complementable Abelian add-associative right_zeroed unital distributive doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for x being Element of L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x)) let p, q be Polynomial of L; ::_thesis: for x being Element of L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x)) let x be Element of L; ::_thesis: eval ((p - q),x) = (eval (p,x)) - (eval (q,x)) thus eval ((p - q),x) = (eval (p,x)) + (eval ((- q),x)) by Th19 .= (eval (p,x)) + (- (eval (q,x))) by Th20 .= (eval (p,x)) - (eval (q,x)) by RLVECT_1:def_11 ; ::_thesis: verum end; theorem Th22: :: POLYNOM4:22 for L being non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr for p being Polynomial of L for x being Element of L holds eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) proof let L be non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L for x being Element of L holds eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) let p be Polynomial of L; ::_thesis: for x being Element of L holds eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) let x be Element of L; ::_thesis: eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) set LMp = Leading-Monomial p; consider F being FinSequence of the carrier of L such that A1: eval ((Leading-Monomial p),x) = Sum F and A2: len F = len (Leading-Monomial p) and A3: for n being Element of NAT st n in dom F holds F . n = ((Leading-Monomial p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; A4: len F = len p by A2, Th15; percases ( len p > 0 or len p = 0 ) ; suppose len p > 0 ; ::_thesis: eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) then A5: len p >= 0 + 1 by NAT_1:13; then len p in Seg (len F) by A4, FINSEQ_1:1; then A6: len p in dom F by FINSEQ_1:def_3; A7: (len p) - 1 >= 0 by A5, XREAL_1:19; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_F_&_i_<>_len_p_holds_ F_/._i_=_0._L A8: (len p) -' 1 = (len p) - 1 by A7, XREAL_0:def_2; let i be Element of NAT ; ::_thesis: ( i in dom F & i <> len p implies F /. i = 0. L ) assume that A9: i in dom F and A10: i <> len p ; ::_thesis: F /. i = 0. L i in Seg (len F) by A9, FINSEQ_1:def_3; then i >= 0 + 1 by FINSEQ_1:1; then i - 1 >= 0 by XREAL_1:19; then i -' 1 = i - 1 by XREAL_0:def_2; then A11: i -' 1 <> (len p) -' 1 by A10, A8; thus F /. i = F . i by A9, PARTFUN1:def_6 .= ((Leading-Monomial p) . (i -' 1)) * ((power L) . (x,(i -' 1))) by A3, A9 .= (0. L) * ((power L) . (x,(i -' 1))) by A11, Def1 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; then Sum F = F /. (len p) by A6, POLYNOM2:3 .= F . (len p) by A6, PARTFUN1:def_6 .= ((Leading-Monomial p) . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) by A3, A6 ; hence eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) by A1, Def1; ::_thesis: verum end; supposeA12: len p = 0 ; ::_thesis: eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) then A13: p = 0_. L by Th5; Leading-Monomial p = 0_. L by A12, Th12; hence eval ((Leading-Monomial p),x) = 0. L by Th17 .= (0. L) * ((power L) . (x,((len p) -' 1))) by VECTSP_1:7 .= (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) by A13, FUNCOP_1:7 ; ::_thesis: verum end; end; end; Lm3: for L being non empty right_complementable add-associative right_zeroed unital associative distributive doubleLoopStr for p, q being Polynomial of L st len p > 0 & len q > 0 holds for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) proof let L be non empty right_complementable add-associative right_zeroed unital associative distributive doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st len p > 0 & len q > 0 holds for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) let p, q be Polynomial of L; ::_thesis: ( len p > 0 & len q > 0 implies for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) ) assume that A1: len p > 0 and A2: len q > 0 ; ::_thesis: for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) A3: len q >= 0 + 1 by A2, NAT_1:13; then A4: (len q) - 1 >= 0 by XREAL_1:19; A5: len p >= 0 + 1 by A1, NAT_1:13; then (len p) - 1 >= 0 by XREAL_1:19; then A6: (len p) - 1 = (len p) -' 1 by XREAL_0:def_2; A7: (len p) + (len q) >= 0 + (1 + 1) by A5, A3, XREAL_1:7; then A8: ((len p) + (len q)) - 1 >= 1 by XREAL_1:19; then reconsider i1 = ((len p) + (len q)) - 1 as Element of NAT by INT_1:3; A9: (i1 -' 1) + 1 = i1 by A8, XREAL_1:235; set LMp = Leading-Monomial p; set LMq = Leading-Monomial q; let x be Element of L; ::_thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) consider F being FinSequence of the carrier of L such that A10: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = Sum F and A11: len F = len ((Leading-Monomial p) *' (Leading-Monomial q)) and A12: for n being Element of NAT st n in dom F holds F . n = (((Leading-Monomial p) *' (Leading-Monomial q)) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2; consider r being FinSequence of the carrier of L such that A13: len r = (i1 -' 1) + 1 and A14: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = Sum r and A15: for k being Element of NAT st k in dom r holds r . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' k)) by POLYNOM3:def_9; (len p) + 0 <= (len p) + ((len q) - 1) by A4, XREAL_1:7; then len p in Seg (len r) by A5, A9, A13, FINSEQ_1:1; then A16: len p in dom r by FINSEQ_1:def_3; ((len p) + ((len q) - 1)) - (len p) >= 0 by A3, XREAL_1:19; then i1 -' (len p) = ((len p) + ((len q) - 1)) - (len p) by XREAL_0:def_2 .= (len q) -' 1 by A4, XREAL_0:def_2 ; then A17: r . (len p) = ((Leading-Monomial p) . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by A9, A15, A16; 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 that A18: i in dom r and A19: i <> len p ; ::_thesis: r /. i = 0. L i in Seg (len r) by A18, FINSEQ_1:def_3; then i >= 0 + 1 by FINSEQ_1:1; then i - 1 >= 0 by XREAL_1:19; then i -' 1 = i - 1 by XREAL_0:def_2; then A20: i -' 1 <> (len p) -' 1 by A6, A19; thus r /. i = r . i by A18, PARTFUN1:def_6 .= ((Leading-Monomial p) . (i -' 1)) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' i)) by A15, A18 .= (0. L) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' i)) by A20, Def1 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; then A21: Sum r = r /. (len p) by A16, POLYNOM2:3 .= ((Leading-Monomial p) . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by A16, A17, PARTFUN1:def_6 .= (p . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by Def1 .= (p . ((len p) -' 1)) * (q . ((len q) -' 1)) by Def1 ; A22: (len q) - 1 = (len q) -' 1 by A4, XREAL_0:def_2; A23: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_F_&_i_<>_i1_holds_ F_/._i_=_0._L let i be Element of NAT ; ::_thesis: ( i in dom F & i <> i1 implies F /. i = 0. L ) assume that A24: i in dom F and A25: i <> i1 ; ::_thesis: F /. i = 0. L consider r1 being FinSequence of the carrier of L such that A26: len r1 = (i -' 1) + 1 and A27: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i -' 1) = Sum r1 and A28: for k being Element of NAT st k in dom r1 holds r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . (((i -' 1) + 1) -' k)) by POLYNOM3:def_9; i in Seg (len F) by A24, FINSEQ_1:def_3; then i >= 1 by FINSEQ_1:1; then A29: (i -' 1) + 1 = i by XREAL_1:235; A30: now__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_r1_holds_ r1_._j_=_0._L let j be Element of NAT ; ::_thesis: ( j in dom r1 implies r1 . b1 = 0. L ) assume A31: j in dom r1 ; ::_thesis: r1 . b1 = 0. L then j in Seg (len r1) by FINSEQ_1:def_3; then j >= 0 + 1 by FINSEQ_1:1; then j - 1 >= 0 by XREAL_1:19; then A32: j -' 1 = j - 1 by XREAL_0:def_2; percases ( j <> len p or j = len p ) ; suppose j <> len p ; ::_thesis: r1 . b1 = 0. L then A33: j -' 1 <> (len p) -' 1 by A6, A32; thus r1 . j = ((Leading-Monomial p) . (j -' 1)) * ((Leading-Monomial q) . (((i -' 1) + 1) -' j)) by A28, A31 .= (0. L) * ((Leading-Monomial q) . (((i -' 1) + 1) -' j)) by A33, Def1 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; supposeA34: j = len p ; ::_thesis: r1 . b1 = 0. L j in Seg (len r1) by A31, FINSEQ_1:def_3; then i >= 0 + j by A26, A29, FINSEQ_1:1; then i - j >= 0 by XREAL_1:19; then i -' (len p) = i - (len p) by A34, XREAL_0:def_2; then A35: i -' (len p) <> (len q) -' 1 by A22, A25; thus r1 . j = ((Leading-Monomial p) . (j -' 1)) * ((Leading-Monomial q) . (i -' (len p))) by A28, A29, A31, A34 .= ((Leading-Monomial p) . (j -' 1)) * (0. L) by A35, Def1 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; end; end; thus F /. i = F . i by A24, PARTFUN1:def_6 .= (Sum r1) * ((power L) . (x,(i -' 1))) by A12, A24, A27 .= (0. L) * ((power L) . (x,(i -' 1))) by A30, POLYNOM3:1 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; A36: ((len p) + (len q)) - 2 >= 0 by A7, XREAL_1:19; ((len p) + (len q)) - (1 + 1) >= 0 by A7, XREAL_1:19; then A37: i1 -' 1 = (((len p) + (len q)) - 1) - 1 by XREAL_0:def_2 .= ((len p) + (len q)) -' 2 by A36, XREAL_0:def_2 ; percases ( ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. L or ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. L ) ; suppose ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. L ; ::_thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) then len F > i1 -' 1 by A11, ALGSEQ_1:8; then len F >= i1 by A9, NAT_1:13; then i1 in Seg (len F) by A8, FINSEQ_1:1; then A38: i1 in dom F by FINSEQ_1:def_3; hence eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = F /. i1 by A10, A23, POLYNOM2:3 .= F . i1 by A38, PARTFUN1:def_6 .= ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) by A12, A14, A37, A21, A38 ; ::_thesis: verum end; supposeA39: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. L ; ::_thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) now__::_thesis:_for_j_being_Nat_st_j_>=_0_holds_ ((Leading-Monomial_p)_*'_(Leading-Monomial_q))_._j_=_0._L let j be Nat; ::_thesis: ( j >= 0 implies ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L ) assume j >= 0 ; ::_thesis: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L j in NAT by ORDINAL1:def_12; then consider r1 being FinSequence of the carrier of L such that A40: len r1 = j + 1 and A41: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = Sum r1 and A42: for k being Element of NAT st k in dom r1 holds r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by POLYNOM3:def_9; now__::_thesis:_((Leading-Monomial_p)_*'_(Leading-Monomial_q))_._j_=_0._L percases ( j = i1 -' 1 or j <> i1 -' 1 ) ; suppose j = i1 -' 1 ; ::_thesis: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L by A39; ::_thesis: verum end; supposeA43: j <> i1 -' 1 ; ::_thesis: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r1_holds_ r1_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom r1 implies r1 . b1 = 0. L ) assume A44: k in dom r1 ; ::_thesis: r1 . b1 = 0. L percases ( k -' 1 <> (len p) -' 1 or k -' 1 = (len p) -' 1 ) ; supposeA45: k -' 1 <> (len p) -' 1 ; ::_thesis: r1 . b1 = 0. L thus r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by A42, A44 .= (0. L) * ((Leading-Monomial q) . ((j + 1) -' k)) by A45, Def1 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; supposeA46: k -' 1 = (len p) -' 1 ; ::_thesis: r1 . b1 = 0. L A47: k in Seg (len r1) by A44, FINSEQ_1:def_3; then 0 + 1 <= k by FINSEQ_1:1; then k - 1 >= 0 by XREAL_1:19; then A48: k -' 1 = k - 1 by XREAL_0:def_2; 0 + k <= j + 1 by A40, A47, FINSEQ_1:1; then (j + 1) - k >= 0 by XREAL_1:19; then A49: (j + 1) -' k = (j - (len p)) + 1 by A6, A46, A48, XREAL_0:def_2; A50: (j - (len p)) + 1 <> ((i1 -' 1) - (len p)) + 1 by A43; thus r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by A42, A44 .= ((Leading-Monomial p) . (k -' 1)) * (0. L) by A22, A9, A49, A50, Def1 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; end; end; hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L by A41, POLYNOM3:1; ::_thesis: verum end; end; end; hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L ; ::_thesis: verum end; then 0 is_at_least_length_of (Leading-Monomial p) *' (Leading-Monomial q) by ALGSEQ_1:def_2; then len ((Leading-Monomial p) *' (Leading-Monomial q)) = 0 by ALGSEQ_1:def_3; then (Leading-Monomial p) *' (Leading-Monomial q) = 0_. L by Th5; then eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = 0. L by Th17; hence eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) by A14, A21, A39, VECTSP_1:7; ::_thesis: verum end; end; end; Lm4: for L being non trivial right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr for p, q being Polynomial of L for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) proof let L be non trivial right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) let p, q be Polynomial of L; ::_thesis: for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) let x be Element of L; ::_thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) percases ( ( len p <> 0 & len q <> 0 ) or len p = 0 or len q = 0 ) ; supposeA1: ( len p <> 0 & len q <> 0 ) ; ::_thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) then A2: len q >= 0 + 1 by NAT_1:13; then (len q) - 1 >= 0 by XREAL_1:19; then A3: (len q) - 1 = (len q) -' 1 by XREAL_0:def_2; A4: len p >= 0 + 1 by A1, NAT_1:13; then (len p) - 1 >= 0 by XREAL_1:19; then A5: (len p) - 1 = (len p) -' 1 by XREAL_0:def_2; (len p) + (len q) >= 0 + (1 + 1) by A4, A2, XREAL_1:7; then ((len p) + (len q)) - 2 >= 0 by XREAL_1:19; then A6: ((len p) + (len q)) -' 2 = ((len p) + (len q)) - 2 by XREAL_0:def_2; A7: ((len p) + (len q)) - (1 + 1) = ((len p) - 1) + ((len q) - 1) ; thus eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) by A1, Lm3 .= ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * (((power L) . (x,((len p) -' 1))) * ((power L) . (x,((len q) -' 1)))) by A5, A3, A6, A7, POLYNOM2:1 .= (p . ((len p) -' 1)) * ((q . ((len q) -' 1)) * (((power L) . (x,((len p) -' 1))) * ((power L) . (x,((len q) -' 1))))) by GROUP_1:def_3 .= (p . ((len p) -' 1)) * (((power L) . (x,((len p) -' 1))) * ((q . ((len q) -' 1)) * ((power L) . (x,((len q) -' 1))))) by GROUP_1:def_3 .= ((p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))) * ((q . ((len q) -' 1)) * ((power L) . (x,((len q) -' 1)))) by GROUP_1:def_3 .= ((p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))) * (eval ((Leading-Monomial q),x)) by Th22 .= (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) by Th22 ; ::_thesis: verum end; suppose len p = 0 ; ::_thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) then A8: Leading-Monomial p = 0_. L by Th12; hence eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = eval ((0_. L),x) by Th2 .= 0. L by Th17 .= (0. L) * (eval ((Leading-Monomial q),x)) by VECTSP_1:7 .= (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) by A8, Th17 ; ::_thesis: verum end; suppose len q = 0 ; ::_thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) then len (Leading-Monomial q) = 0 by Th15; then A9: Leading-Monomial q = 0_. L by Th5; hence eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = eval ((0_. L),x) by POLYNOM3:34 .= 0. L by Th17 .= (eval ((Leading-Monomial p),x)) * (0. L) by VECTSP_1:7 .= (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) by A9, Th17 ; ::_thesis: verum end; end; end; theorem Th23: :: POLYNOM4:23 for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr for p, q being Polynomial of L for x being Element of L holds eval (((Leading-Monomial p) *' q),x) = (eval ((Leading-Monomial p),x)) * (eval (q,x)) proof let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for x being Element of L holds eval (((Leading-Monomial p) *' q),x) = (eval ((Leading-Monomial p),x)) * (eval (q,x)) let p1, q be Polynomial of L; ::_thesis: for x being Element of L holds eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) let x be Element of L; ::_thesis: eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) set p = Leading-Monomial p1; defpred S1[ Nat] means for q being Polynomial of L st len q = $1 holds eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)); A1: for k being Nat st ( for n being Nat st n < k holds S1[n] ) holds S1[k] proof let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds S1[n] ) implies S1[k] ) assume A2: for n being Nat st n < k holds for q being Polynomial of L st len q = n holds eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) ; ::_thesis: S1[k] let q be Polynomial of L; ::_thesis: ( len q = k implies eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) ) assume A3: len q = k ; ::_thesis: eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) percases ( len q <> 0 or len q = 0 ) ; supposeA4: len q <> 0 ; ::_thesis: eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) set LMq = Leading-Monomial q; consider r being Polynomial of L such that A5: len r < len q and A6: q = r + (Leading-Monomial q) and for n being Element of NAT st n < (len q) - 1 holds r . n = q . n by A4, Th16; thus eval (((Leading-Monomial p1) *' q),x) = eval ((((Leading-Monomial p1) *' r) + ((Leading-Monomial p1) *' (Leading-Monomial q))),x) by A6, POLYNOM3:31 .= (eval (((Leading-Monomial p1) *' r),x)) + (eval (((Leading-Monomial p1) *' (Leading-Monomial q)),x)) by Th19 .= ((eval ((Leading-Monomial p1),x)) * (eval (r,x))) + (eval (((Leading-Monomial p1) *' (Leading-Monomial q)),x)) by A2, A3, A5 .= ((eval ((Leading-Monomial p1),x)) * (eval (r,x))) + ((eval ((Leading-Monomial p1),x)) * (eval ((Leading-Monomial q),x))) by Lm4 .= (eval ((Leading-Monomial p1),x)) * ((eval (r,x)) + (eval ((Leading-Monomial q),x))) by VECTSP_1:def_7 .= (eval ((Leading-Monomial p1),x)) * (eval (q,x)) by A6, Th19 ; ::_thesis: verum end; suppose len q = 0 ; ::_thesis: eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) then A7: q = 0_. L by Th5; hence eval (((Leading-Monomial p1) *' q),x) = eval ((0_. L),x) by POLYNOM3:34 .= 0. L by Th17 .= (eval ((Leading-Monomial p1),x)) * (0. L) by VECTSP_1:7 .= (eval ((Leading-Monomial p1),x)) * (eval (q,x)) by A7, Th17 ; ::_thesis: verum end; end; end; A8: for n being Nat holds S1[n] from NAT_1:sch_4(A1); len q = len q ; hence eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) by A8; ::_thesis: verum end; theorem Th24: :: POLYNOM4:24 for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr for p, q being Polynomial of L for x being Element of L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) proof let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ; ::_thesis: for p, q being Polynomial of L for x being Element of L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) let p, q be Polynomial of L; ::_thesis: for x being Element of L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) let x be Element of L; ::_thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) defpred S1[ Nat] means for p being Polynomial of L st len p = $1 holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)); A1: for k being Nat st ( for n being Nat st n < k holds S1[n] ) holds S1[k] proof let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds S1[n] ) implies S1[k] ) assume A2: for n being Nat st n < k holds for p being Polynomial of L st len p = n holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) ; ::_thesis: S1[k] let p be Polynomial of L; ::_thesis: ( len p = k implies eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) ) assume A3: len p = k ; ::_thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) percases ( len p <> 0 or len p = 0 ) ; supposeA4: len p <> 0 ; ::_thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) set LMp = Leading-Monomial p; consider r being Polynomial of L such that A5: len r < len p and A6: p = r + (Leading-Monomial p) and for n being Element of NAT st n < (len p) - 1 holds r . n = p . n by A4, Th16; thus eval ((p *' q),x) = eval (((r *' q) + ((Leading-Monomial p) *' q)),x) by A6, POLYNOM3:32 .= (eval ((r *' q),x)) + (eval (((Leading-Monomial p) *' q),x)) by Th19 .= ((eval (r,x)) * (eval (q,x))) + (eval (((Leading-Monomial p) *' q),x)) by A2, A3, A5 .= ((eval (r,x)) * (eval (q,x))) + ((eval ((Leading-Monomial p),x)) * (eval (q,x))) by Th23 .= ((eval (r,x)) + (eval ((Leading-Monomial p),x))) * (eval (q,x)) by VECTSP_1:def_7 .= (eval (p,x)) * (eval (q,x)) by A6, Th19 ; ::_thesis: verum end; suppose len p = 0 ; ::_thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) then A7: p = 0_. L by Th5; hence eval ((p *' q),x) = eval ((0_. L),x) by Th2 .= 0. L by Th17 .= (0. L) * (eval (q,x)) by VECTSP_1:7 .= (eval (p,x)) * (eval (q,x)) by A7, Th17 ; ::_thesis: verum end; end; end; A8: for n being Nat holds S1[n] from NAT_1:sch_4(A1); len p = len p ; hence eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) by A8; ::_thesis: verum end; begin definition let L be non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr ; let x be Element of L; func Polynom-Evaluation (L,x) -> Function of (Polynom-Ring L),L means :Def3: :: POLYNOM4:def 3 for p being Polynomial of L holds it . p = eval (p,x); existence ex b1 being Function of (Polynom-Ring L),L st for p being Polynomial of L holds b1 . p = eval (p,x) proof defpred S1[ set , set ] means ex p being Polynomial of L st ( p = $1 & $2 = eval (p,x) ); A1: for y being Element of (Polynom-Ring L) ex z being Element of L st S1[y,z] proof let y be Element of (Polynom-Ring L); ::_thesis: ex z being Element of L st S1[y,z] reconsider p = y as Polynomial of L by POLYNOM3:def_10; take eval (p,x) ; ::_thesis: S1[y, eval (p,x)] take p ; ::_thesis: ( p = y & eval (p,x) = eval (p,x) ) thus ( p = y & eval (p,x) = eval (p,x) ) ; ::_thesis: verum end; consider f being Function of the carrier of (Polynom-Ring L), the carrier of L such that A2: for y being Element of (Polynom-Ring L) holds S1[y,f . y] from FUNCT_2:sch_3(A1); reconsider f = f as Function of (Polynom-Ring L),L ; take f ; ::_thesis: for p being Polynomial of L holds f . p = eval (p,x) let p be Polynomial of L; ::_thesis: f . p = eval (p,x) p in the carrier of (Polynom-Ring L) by POLYNOM3:def_10; then ex q being Polynomial of L st ( q = p & f . p = eval (q,x) ) by A2; hence f . p = eval (p,x) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Polynom-Ring L),L st ( for p being Polynomial of L holds b1 . p = eval (p,x) ) & ( for p being Polynomial of L holds b2 . p = eval (p,x) ) holds b1 = b2 proof let f1, f2 be Function of (Polynom-Ring L),L; ::_thesis: ( ( for p being Polynomial of L holds f1 . p = eval (p,x) ) & ( for p being Polynomial of L holds f2 . p = eval (p,x) ) implies f1 = f2 ) assume that A3: for p being Polynomial of L holds f1 . p = eval (p,x) and A4: for p being Polynomial of L holds f2 . p = eval (p,x) ; ::_thesis: f1 = f2 now__::_thesis:_for_y_being_Element_of_(Polynom-Ring_L)_holds_f1_._y_=_f2_._y let y be Element of (Polynom-Ring L); ::_thesis: f1 . y = f2 . y reconsider p = y as Polynomial of L by POLYNOM3:def_10; thus f1 . y = eval (p,x) by A3 .= f2 . y by A4 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines Polynom-Evaluation POLYNOM4:def_3_:_ for L being non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr for x being Element of L for b3 being Function of (Polynom-Ring L),L holds ( b3 = Polynom-Evaluation (L,x) iff for p being Polynomial of L holds b3 . p = eval (p,x) ); registration let L be non empty non degenerated right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; let x be Element of L; cluster Polynom-Evaluation (L,x) -> unity-preserving ; coherence Polynom-Evaluation (L,x) is unity-preserving proof thus (Polynom-Evaluation (L,x)) . (1_ (Polynom-Ring L)) = (Polynom-Evaluation (L,x)) . (1_. L) by POLYNOM3:36 .= eval ((1_. L),x) by Def3 .= 1_ L by Th18 ; :: according to GROUP_1:def_13 ::_thesis: verum end; end; registration let L be non empty right_complementable Abelian add-associative right_zeroed unital distributive doubleLoopStr ; let x be Element of L; cluster Polynom-Evaluation (L,x) -> additive ; coherence Polynom-Evaluation (L,x) is additive proof let a, b be Element of (Polynom-Ring L); :: according to VECTSP_1:def_20 ::_thesis: (Polynom-Evaluation (L,x)) . (a + b) = ((Polynom-Evaluation (L,x)) . a) + ((Polynom-Evaluation (L,x)) . b) reconsider p = a, q = b as Polynomial of L by POLYNOM3:def_10; thus (Polynom-Evaluation (L,x)) . (a + b) = (Polynom-Evaluation (L,x)) . (p + q) by POLYNOM3:def_10 .= eval ((p + q),x) by Def3 .= (eval (p,x)) + (eval (q,x)) by Th19 .= ((Polynom-Evaluation (L,x)) . a) + (eval (q,x)) by Def3 .= ((Polynom-Evaluation (L,x)) . a) + ((Polynom-Evaluation (L,x)) . b) by Def3 ; ::_thesis: verum end; end; registration let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ; let x be Element of L; cluster Polynom-Evaluation (L,x) -> multiplicative ; coherence Polynom-Evaluation (L,x) is multiplicative proof let a, b be Element of (Polynom-Ring L); :: according to GROUP_6:def_6 ::_thesis: (Polynom-Evaluation (L,x)) . (a * b) = ((Polynom-Evaluation (L,x)) . a) * ((Polynom-Evaluation (L,x)) . b) reconsider p = a, q = b as Polynomial of L by POLYNOM3:def_10; thus (Polynom-Evaluation (L,x)) . (a * b) = (Polynom-Evaluation (L,x)) . (p *' q) by POLYNOM3:def_10 .= eval ((p *' q),x) by Def3 .= (eval (p,x)) * (eval (q,x)) by Th24 .= ((Polynom-Evaluation (L,x)) . a) * (eval (q,x)) by Def3 .= ((Polynom-Evaluation (L,x)) . a) * ((Polynom-Evaluation (L,x)) . b) by Def3 ; ::_thesis: verum end; end; registration let L be non empty non degenerated right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; let x be Element of L; cluster Polynom-Evaluation (L,x) -> RingHomomorphism ; coherence Polynom-Evaluation (L,x) is RingHomomorphism proof thus ( Polynom-Evaluation (L,x) is additive & Polynom-Evaluation (L,x) is multiplicative & Polynom-Evaluation (L,x) is unity-preserving ) ; :: according to QUOFIELD:def_18 ::_thesis: verum end; end;