:: by Robert Milewski

::

:: Received April 17, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

theorem Th1: :: POLYNOM3:1

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds

p . i = 0. L ) holds

Sum p = 0. L

for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds

p . i = 0. L ) holds

Sum p = 0. L

proof end;

theorem Th2: :: POLYNOM3:2

for V being non empty Abelian add-associative right_zeroed addLoopStr

for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p)

for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p)

proof end;

definition

let D be non empty set ;

let i be Element of NAT ;

let p be FinSequence of D;

:: original: Del

redefine func Del (p,i) -> FinSequence of D;

coherence

Del (p,i) is FinSequence of D by FINSEQ_3:105;

end;
let i be Element of NAT ;

let p be FinSequence of D;

:: original: Del

redefine func Del (p,i) -> FinSequence of D;

coherence

Del (p,i) is FinSequence of D by FINSEQ_3:105;

definition

let D be non empty set ;

let a, b be Element of D;

:: original: <*

redefine func <*a,b*> -> Element of 2 -tuples_on D;

coherence

<*a,b*> is Element of 2 -tuples_on D by FINSEQ_2:101;

end;
let a, b be Element of D;

:: original: <*

redefine func <*a,b*> -> Element of 2 -tuples_on D;

coherence

<*a,b*> is Element of 2 -tuples_on D by FINSEQ_2:101;

definition

let D be non empty set ;

let k, n be Element of NAT ;

let p be Element of k -tuples_on D;

let q be Element of n -tuples_on D;

:: original: ^

redefine func p ^ q -> Element of (k + n) -tuples_on D;

coherence

p ^ q is Element of (k + n) -tuples_on D

end;
let k, n be Element of NAT ;

let p be Element of k -tuples_on D;

let q be Element of n -tuples_on D;

:: original: ^

redefine func p ^ q -> Element of (k + n) -tuples_on D;

coherence

p ^ q is Element of (k + n) -tuples_on D

proof end;

definition

let D be non empty set ;

let k, n be Element of NAT ;

let p be FinSequence of k -tuples_on D;

let q be FinSequence of n -tuples_on D;

:: original: ^^

redefine func p ^^ q -> Element of ((k + n) -tuples_on D) * ;

coherence

p ^^ q is Element of ((k + n) -tuples_on D) *

end;
let k, n be Element of NAT ;

let p be FinSequence of k -tuples_on D;

let q be FinSequence of n -tuples_on D;

:: original: ^^

redefine func p ^^ q -> Element of ((k + n) -tuples_on D) * ;

coherence

p ^^ q is Element of ((k + n) -tuples_on D) *

proof end;

scheme :: POLYNOM3:sch 1

SeqOfSeqLambdaD{ F_{1}() -> non empty set , F_{2}() -> Element of NAT , F_{3}( Element of NAT ) -> Element of NAT , F_{4}( set , set ) -> Element of F_{1}() } :

SeqOfSeqLambdaD{ F

ex p being FinSequence of F_{1}() * st

( len p = F_{2}() & ( for k being Element of NAT st k in Seg F_{2}() holds

( len (p /. k) = F_{3}(k) & ( for n being Element of NAT st n in dom (p /. k) holds

(p /. k) . n = F_{4}(k,n) ) ) ) )

( len p = F

( len (p /. k) = F

(p /. k) . n = F

proof end;

begin

definition

let n be Element of NAT ;

let p, q be Element of n -tuples_on NAT;

for p, q being Element of n -tuples_on NAT st ex i being Element of NAT st

( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds

p . k = q . k ) ) holds

for i being Element of NAT holds

( not i in Seg n or not q . i < p . i or ex k being Element of NAT st

( 1 <= k & k < i & not q . k = p . k ) )

end;
let p, q be Element of n -tuples_on NAT;

pred p < q means :Def1: :: POLYNOM3:def 1

ex i being Element of NAT st

( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds

p . k = q . k ) );

asymmetry ex i being Element of NAT st

( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds

p . k = q . k ) );

for p, q being Element of n -tuples_on NAT st ex i being Element of NAT st

( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds

p . k = q . k ) ) holds

for i being Element of NAT holds

( not i in Seg n or not q . i < p . i or ex k being Element of NAT st

( 1 <= k & k < i & not q . k = p . k ) )

proof end;

:: deftheorem Def1 defines < POLYNOM3:def 1 :

for n being Element of NAT

for p, q being Element of n -tuples_on NAT holds

( p < q iff ex i being Element of NAT st

( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds

p . k = q . k ) ) );

for n being Element of NAT

for p, q being Element of n -tuples_on NAT holds

( p < q iff ex i being Element of NAT st

( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds

p . k = q . k ) ) );

notation
end;

definition

let n be Element of NAT ;

let p, q be Element of n -tuples_on NAT;

reflexivity

for p being Element of n -tuples_on NAT holds

( p < p or p = p ) ;

end;
let p, q be Element of n -tuples_on NAT;

reflexivity

for p being Element of n -tuples_on NAT holds

( p < p or p = p ) ;

:: deftheorem Def2 defines <= POLYNOM3:def 2 :

for n being Element of NAT

for p, q being Element of n -tuples_on NAT holds

( p <= q iff ( p < q or p = q ) );

for n being Element of NAT

for p, q being Element of n -tuples_on NAT holds

( p <= q iff ( p < q or p = q ) );

notation
end;

theorem Th5: :: POLYNOM3:5

for n being Element of NAT

for p, q, r being Element of n -tuples_on NAT holds

( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

for p, q, r being Element of n -tuples_on NAT holds

( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

proof end;

theorem Th6: :: POLYNOM3:6

for n being Element of NAT

for p, q being Element of n -tuples_on NAT st p <> q holds

ex i being Element of NAT st

( i in Seg n & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds

p . k = q . k ) )

for p, q being Element of n -tuples_on NAT st p <> q holds

ex i being Element of NAT st

( i in Seg n & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds

p . k = q . k ) )

proof end;

definition

let n be Element of NAT ;

ex b_{1} being Order of (n -tuples_on NAT) st

for p, q being Element of n -tuples_on NAT holds

( [p,q] in b_{1} iff p <= q )

for b_{1}, b_{2} being Order of (n -tuples_on NAT) st ( for p, q being Element of n -tuples_on NAT holds

( [p,q] in b_{1} iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds

( [p,q] in b_{2} iff p <= q ) ) holds

b_{1} = b_{2}

end;
func TuplesOrder n -> Order of (n -tuples_on NAT) means :Def3: :: POLYNOM3:def 3

for p, q being Element of n -tuples_on NAT holds

( [p,q] in it iff p <= q );

existence for p, q being Element of n -tuples_on NAT holds

( [p,q] in it iff p <= q );

ex b

for p, q being Element of n -tuples_on NAT holds

( [p,q] in b

proof end;

uniqueness for b

( [p,q] in b

( [p,q] in b

b

proof end;

:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :

for n being Element of NAT

for b_{2} being Order of (n -tuples_on NAT) holds

( b_{2} = TuplesOrder n iff for p, q being Element of n -tuples_on NAT holds

( [p,q] in b_{2} iff p <= q ) );

for n being Element of NAT

for b

( b

( [p,q] in b

registration
end;

begin

definition

let i be non empty Element of NAT ;

let n be Element of NAT ;

ex b_{1} being FinSequence of i -tuples_on NAT ex A being finite Subset of (i -tuples_on NAT) st

( b_{1} = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds

( p in A iff Sum p = n ) ) )

for b_{1}, b_{2} being FinSequence of i -tuples_on NAT st ex A being finite Subset of (i -tuples_on NAT) st

( b_{1} = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds

( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT) st

( b_{2} = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds

( p in A iff Sum p = n ) ) ) holds

b_{1} = b_{2}

end;
let n be Element of NAT ;

func Decomp (n,i) -> FinSequence of i -tuples_on NAT means :Def4: :: POLYNOM3:def 4

ex A being finite Subset of (i -tuples_on NAT) st

( it = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds

( p in A iff Sum p = n ) ) );

existence ex A being finite Subset of (i -tuples_on NAT) st

( it = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds

( p in A iff Sum p = n ) ) );

ex b

( b

( p in A iff Sum p = n ) ) )

proof end;

uniqueness for b

( b

( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT) st

( b

( p in A iff Sum p = n ) ) ) holds

b

proof end;

:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :

for i being non empty Element of NAT

for n being Element of NAT

for b_{3} being FinSequence of i -tuples_on NAT holds

( b_{3} = Decomp (n,i) iff ex A being finite Subset of (i -tuples_on NAT) st

( b_{3} = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds

( p in A iff Sum p = n ) ) ) );

for i being non empty Element of NAT

for n being Element of NAT

for b

( b

( b

( p in A iff Sum p = n ) ) ) );

registration

let i be non empty Element of NAT ;

let n be Element of NAT ;

coherence

( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding )

end;
let n be Element of NAT ;

coherence

( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding )

proof end;

theorem Th11: :: POLYNOM3:11

for i, j, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> holds

( i < j iff k1 < k2 )

( i < j iff k1 < k2 )

proof end;

theorem Th12: :: POLYNOM3:12

for i, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> holds

k2 = k1 + 1

k2 = k1 + 1

proof end;

theorem Th14: :: POLYNOM3:14

for n, i being Element of NAT st i in Seg (n + 1) holds

(Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>

(Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>

proof end;

definition

let L be non empty multMagma ;

let p, q, r be sequence of L;

let t be FinSequence of 3 -tuples_on NAT;

ex b_{1} being Element of the carrier of L * st

( len b_{1} = len t & ( for k being Element of NAT st k in dom t holds

b_{1} . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )

for b_{1}, b_{2} being Element of the carrier of L * st len b_{1} = len t & ( for k being Element of NAT st k in dom t holds

b_{1} . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) & len b_{2} = len t & ( for k being Element of NAT st k in dom t holds

b_{2} . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) holds

b_{1} = b_{2}

end;
let p, q, r be sequence of L;

let t be FinSequence of 3 -tuples_on NAT;

func prodTuples (p,q,r,t) -> Element of the carrier of L * means :Def5: :: POLYNOM3:def 5

( len it = len t & ( for k being Element of NAT st k in dom t holds

it . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) );

existence ( len it = len t & ( for k being Element of NAT st k in dom t holds

it . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines prodTuples POLYNOM3:def 5 :

for L being non empty multMagma

for p, q, r being sequence of L

for t being FinSequence of 3 -tuples_on NAT

for b_{6} being Element of the carrier of L * holds

( b_{6} = prodTuples (p,q,r,t) iff ( len b_{6} = len t & ( for k being Element of NAT st k in dom t holds

b_{6} . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) );

for L being non empty multMagma

for p, q, r being sequence of L

for t being FinSequence of 3 -tuples_on NAT

for b

( b

b

theorem Th15: :: POLYNOM3:15

for L being non empty multMagma

for p, q, r being sequence of L

for t being FinSequence of 3 -tuples_on NAT

for P being Permutation of (dom t)

for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds

prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P

for p, q, r being sequence of L

for t being FinSequence of 3 -tuples_on NAT

for P being Permutation of (dom t)

for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds

prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P

proof end;

theorem Th16: :: POLYNOM3:16

for D being set

for f being FinSequence of D *

for i being Element of NAT holds Card (f | i) = (Card f) | i

for f being FinSequence of D *

for i being Element of NAT holds Card (f | i) = (Card f) | i

proof end;

theorem :: POLYNOM3:17

for p being FinSequence of REAL

for q being FinSequence of NAT st p = q holds

for i being Element of NAT holds p | i = q | i ;

for q being FinSequence of NAT st p = q holds

for i being Element of NAT holds p | i = q | i ;

theorem Th18: :: POLYNOM3:18

for p being FinSequence of NAT

for i, j being Element of NAT st i <= j holds

Sum (p | i) <= Sum (p | j)

for i, j being Element of NAT st i <= j holds

Sum (p | i) <= Sum (p | j)

proof end;

theorem :: POLYNOM3:19

theorem Th20: :: POLYNOM3:20

for p being FinSequence of REAL

for i being Element of NAT st i < len p holds

Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))

for i being Element of NAT st i < len p holds

Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))

proof end;

theorem Th21: :: POLYNOM3:21

for p being FinSequence of NAT

for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds

( i = j & k1 = k2 )

for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds

( i = j & k1 = k2 )

proof end;

theorem Th22: :: POLYNOM3:22

for D1, D2 being set

for f1 being FinSequence of D1 *

for f2 being FinSequence of D2 *

for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds

( i1 = i2 & j1 = j2 )

for f1 being FinSequence of D1 *

for f2 being FinSequence of D2 *

for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds

( i1 = i2 & j1 = j2 )

proof end;

begin

theorem Th23: :: POLYNOM3:23

for L being non empty ZeroStr

for p being Polynomial of L

for n being Element of NAT holds

( n >= len p iff n is_at_least_length_of p )

for p being Polynomial of L

for n being Element of NAT holds

( n >= len p iff n is_at_least_length_of p )

proof end;

registration

let L be non empty right_zeroed addLoopStr ;

let p, q be Polynomial of L;

coherence

p + q is finite-Support

end;
let p, q be Polynomial of L;

coherence

p + q is finite-Support

proof end;

theorem Th24: :: POLYNOM3:24

for L being non empty right_zeroed addLoopStr

for p, q being Polynomial of L

for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds

n is_at_least_length_of p + q

for p, q being Polynomial of L

for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds

n is_at_least_length_of p + q

proof end;

theorem :: POLYNOM3:25

for L being non empty right_zeroed addLoopStr

for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q)

for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q)

proof end;

definition

let L be non empty Abelian addLoopStr ;

let p, q be sequence of L;

:: original: +

redefine func p + q -> Element of bool [:NAT, the carrier of L:];

commutativity

for p, q being sequence of L holds p + q = q + p

end;
let p, q be sequence of L;

:: original: +

redefine func p + q -> Element of bool [:NAT, the carrier of L:];

commutativity

for p, q being sequence of L holds p + q = q + p

proof end;

theorem Th26: :: POLYNOM3:26

for L being non empty add-associative addLoopStr

for p, q, r being sequence of L holds (p + q) + r = p + (q + r)

for p, q, r being sequence of L holds (p + q) + r = p + (q + r)

proof end;

registration

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

let p be Polynomial of L;

coherence

- p is finite-Support

end;
let p be Polynomial of L;

coherence

- p is finite-Support

proof end;

Lm1: for L being non empty addLoopStr

for p, q being sequence of L holds p - q = p + (- q)

proof end;

definition

let L be non empty addLoopStr ;

let p, q be sequence of L;

compatibility

for b_{1} being Element of bool [:NAT, the carrier of L:] holds

( b_{1} = p - q iff b_{1} = p + (- q) )
by Lm1;

end;
let p, q be sequence of L;

compatibility

for b

( b

:: deftheorem defines - POLYNOM3:def 6 :

for L being non empty addLoopStr

for p, q being sequence of L holds p - q = p + (- q);

for L being non empty addLoopStr

for p, q being sequence of L holds p - q = p + (- q);

registration

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

let p, q be Polynomial of L;

coherence

p - q is finite-Support ;

end;
let p, q be Polynomial of L;

coherence

p - q is finite-Support ;

theorem :: POLYNOM3:27

:: deftheorem defines 0_. POLYNOM3:def 7 :

for L being non empty ZeroStr holds 0_. L = NAT --> (0. L);

for L being non empty ZeroStr holds 0_. L = NAT --> (0. L);

theorem Th29: :: POLYNOM3:29

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being sequence of L holds p - p = 0_. L

for p being sequence of L holds p - p = 0_. L

proof end;

definition
end;

:: deftheorem defines 1_. POLYNOM3:def 8 :

for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* (0,(1. L));

for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* (0,(1. L));

theorem Th30: :: POLYNOM3:30

for L being non empty multLoopStr_0 holds

( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds

(1_. L) . n = 0. L ) )

( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds

(1_. L) . n = 0. L ) )

proof end;

definition

let L be non empty doubleLoopStr ;

let p, q be sequence of L;

ex b_{1} being sequence of L st

for i being Element of NAT ex r being FinSequence of the carrier of L st

( len r = i + 1 & b_{1} . i = Sum r & ( for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )

for b_{1}, b_{2} being sequence of L st ( for i being Element of NAT ex r being FinSequence of the carrier of L st

( len r = i + 1 & b_{1} . i = Sum r & ( for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Element of NAT ex r being FinSequence of the carrier of L st

( len r = i + 1 & b_{2} . i = Sum r & ( for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) holds

b_{1} = b_{2}

end;
let p, q be sequence of L;

func p *' q -> sequence of L means :Def9: :: POLYNOM3:def 9

for i being Element of NAT ex r being FinSequence of the carrier of L st

( len r = i + 1 & it . i = Sum r & ( for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) );

existence for i being Element of NAT ex r being FinSequence of the carrier of L st

( len r = i + 1 & it . i = Sum r & ( for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) );

ex b

for i being Element of NAT ex r being FinSequence of the carrier of L st

( len r = i + 1 & b

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )

proof end;

uniqueness for b

( len r = i + 1 & b

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Element of NAT ex r being FinSequence of the carrier of L st

( len r = i + 1 & b

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) holds

b

proof end;

:: deftheorem Def9 defines *' POLYNOM3:def 9 :

for L being non empty doubleLoopStr

for p, q, b_{4} being sequence of L holds

( b_{4} = p *' q iff for i being Element of NAT ex r being FinSequence of the carrier of L st

( len r = i + 1 & b_{4} . i = Sum r & ( for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) );

for L being non empty doubleLoopStr

for p, q, b

( b

( len r = i + 1 & b

r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) );

registration

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

let p, q be Polynomial of L;

coherence

p *' q is finite-Support

end;
let p, q be Polynomial of L;

coherence

p *' q is finite-Support

proof end;

theorem Th31: :: POLYNOM3:31

for L being non empty right_complementable right-distributive Abelian add-associative right_zeroed doubleLoopStr

for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)

for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)

proof end;

theorem Th32: :: POLYNOM3:32

for L being non empty right_complementable left-distributive Abelian add-associative right_zeroed doubleLoopStr

for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)

for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)

proof end;

definition

let n be Element of NAT ;

:: original: <*

redefine func <*n*> -> Element of 1 -tuples_on NAT;

coherence

<*n*> is Element of 1 -tuples_on NAT

end;
:: original: <*

redefine func <*n*> -> Element of 1 -tuples_on NAT;

coherence

<*n*> is Element of 1 -tuples_on NAT

proof end;

theorem Th33: :: POLYNOM3:33

for L being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr

for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)

for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)

proof end;

definition

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

let p, q be sequence of L;

:: original: *'

redefine func p *' q -> sequence of L;

commutativity

for p, q being sequence of L holds p *' q = q *' p

end;
let p, q be sequence of L;

:: original: *'

redefine func p *' q -> sequence of L;

commutativity

for p, q being sequence of L holds p *' q = q *' p

proof end;

theorem :: POLYNOM3:34

for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for p being sequence of L holds p *' (0_. L) = 0_. L

for p being sequence of L holds p *' (0_. L) = 0_. L

proof end;

theorem Th35: :: POLYNOM3:35

for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr

for p being sequence of L holds p *' (1_. L) = p

for p being sequence of L holds p *' (1_. L) = p

proof end;

begin

definition

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

ex b_{1} being non empty strict doubleLoopStr st

( ( for x being set holds

( x in the carrier of b_{1} iff x is Polynomial of L ) ) & ( for x, y being Element of b_{1}

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{1}

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. b_{1} = 0_. L & 1. b_{1} = 1_. L )

for b_{1}, b_{2} being non empty strict doubleLoopStr st ( for x being set holds

( x in the carrier of b_{1} iff x is Polynomial of L ) ) & ( for x, y being Element of b_{1}

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{1}

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. b_{1} = 0_. L & 1. b_{1} = 1_. L & ( for x being set holds

( x in the carrier of b_{2} iff x is Polynomial of L ) ) & ( for x, y being Element of b_{2}

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{2}

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. b_{2} = 0_. L & 1. b_{2} = 1_. L holds

b_{1} = b_{2}

end;
func Polynom-Ring L -> non empty strict doubleLoopStr means :Def10: :: POLYNOM3:def 10

( ( for x being set holds

( x in the carrier of it iff x is Polynomial of L ) ) & ( for x, y being Element of it

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of it

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. it = 0_. L & 1. it = 1_. L );

existence ( ( for x being set holds

( x in the carrier of it iff x is Polynomial of L ) ) & ( for x, y being Element of it

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of it

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. it = 0_. L & 1. it = 1_. L );

ex b

( ( for x being set holds

( x in the carrier of b

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. b

proof end;

uniqueness for b

( x in the carrier of b

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. b

( x in the carrier of b

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. b

b

proof end;

:: deftheorem Def10 defines Polynom-Ring POLYNOM3:def 10 :

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for b_{2} being non empty strict doubleLoopStr holds

( b_{2} = Polynom-Ring L iff ( ( for x being set holds

( x in the carrier of b_{2} iff x is Polynomial of L ) ) & ( for x, y being Element of b_{2}

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b_{2}

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. b_{2} = 0_. L & 1. b_{2} = 1_. L ) );

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for b

( b

( x in the carrier of b

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of b

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. b

registration

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

coherence

Polynom-Ring L is Abelian

end;
coherence

Polynom-Ring L is Abelian

proof end;

registration

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

coherence

Polynom-Ring L is add-associative

Polynom-Ring L is right_zeroed

Polynom-Ring L is right_complementable

end;
coherence

Polynom-Ring L is add-associative

proof end;

coherence Polynom-Ring L is right_zeroed

proof end;

coherence Polynom-Ring L is right_complementable

proof end;

registration

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

coherence

Polynom-Ring L is commutative

end;
coherence

Polynom-Ring L is commutative

proof end;

registration

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

coherence

Polynom-Ring L is associative

end;
coherence

Polynom-Ring L is associative

proof end;

Lm2: now :: thesis: for L being non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr

for x, e being Element of (Polynom-Ring L) st e = 1. (Polynom-Ring L) holds

( x * e = x & e * x = x )

for x, e being Element of (Polynom-Ring L) st e = 1. (Polynom-Ring L) holds

( x * e = x & e * x = x )

let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for x, e being Element of (Polynom-Ring L) st e = 1. (Polynom-Ring L) holds

( x * e = x & e * x = x )

set Pm = Polynom-Ring L;

let x, e be Element of (Polynom-Ring L); :: thesis: ( e = 1. (Polynom-Ring L) implies ( x * e = x & e * x = x ) )

reconsider p = x as Polynomial of L by Def10;

assume A1: e = 1. (Polynom-Ring L) ; :: thesis: ( x * e = x & e * x = x )

A2: 1. (Polynom-Ring L) = 1_. L by Def10;

hence x * e = p *' (1_. L) by A1, Def10

.= x by Th35 ;

:: thesis: e * x = x

thus e * x = p *' (1_. L) by A1, A2, Def10

.= x by Th35 ; :: thesis: verum

end;
( x * e = x & e * x = x )

set Pm = Polynom-Ring L;

let x, e be Element of (Polynom-Ring L); :: thesis: ( e = 1. (Polynom-Ring L) implies ( x * e = x & e * x = x ) )

reconsider p = x as Polynomial of L by Def10;

assume A1: e = 1. (Polynom-Ring L) ; :: thesis: ( x * e = x & e * x = x )

A2: 1. (Polynom-Ring L) = 1_. L by Def10;

hence x * e = p *' (1_. L) by A1, Def10

.= x by Th35 ;

:: thesis: e * x = x

thus e * x = p *' (1_. L) by A1, A2, Def10

.= x by Th35 ; :: thesis: verum

registration

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

coherence

Polynom-Ring L is well-unital

end;
coherence

Polynom-Ring L is well-unital

proof end;

registration

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

coherence

Polynom-Ring L is distributive

end;
coherence

Polynom-Ring L is distributive

proof end;

theorem :: POLYNOM3:36

for L being non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr holds 1. (Polynom-Ring L) = 1_. L by Def10;