let n be Ordinal; :: thesis: for T being connected TermOrder of n

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

for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let T be connected TermOrder of n; :: thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let f be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f implies for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L )

assume A1: A is_MonomialRepresentation_of f ; :: thesis: for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let b be bag of n; :: thesis: ( ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) implies f . b = 0. L )

assume A2: for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ; :: thesis: f . b = 0. L

defpred S_{1}[ Nat] means for f being Polynomial of n,L

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = Sum A & len A = $1 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L;

_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A21, A3);

A24: ex n being Element of NAT st n = len A ;

thus f . b = 0. L by A1, A2, A23, A24; :: thesis: verum

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

for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let T be connected TermOrder of n; :: thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let f be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f implies for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L )

assume A1: A is_MonomialRepresentation_of f ; :: thesis: for b being bag of n st ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let b be bag of n; :: thesis: ( ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) implies f . b = 0. L )

assume A2: for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ; :: thesis: f . b = 0. L

defpred S

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = Sum A & len A = $1 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L;

A3: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A21:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

for f being Polynomial of n,L

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = Sum A & len A = k + 1 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L_{1}[k + 1]
; :: thesis: verum

end;assume A4: S

for f being Polynomial of n,L

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = Sum A & len A = k + 1 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

proof

hence
S
let f be Polynomial of n,L; :: thesis: for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = Sum A & len A = k + 1 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f & f = Sum A & len A = k + 1 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) implies f . b = 0. L )

assume that

A5: A is_MonomialRepresentation_of f and

A6: f = Sum A and

A7: len A = k + 1 ; :: thesis: ( ex i being Element of NAT st

( i in dom A & ex m being Monomial of n,L ex p being Polynomial of n,L st

( A . i = m *' p & p in P & not (m *' p) . b = 0. L ) ) or f . b = 0. L )

set B = A | (Seg k);

reconsider B = A | (Seg k) as FinSequence of (Polynom-Ring (n,L)) by FINSEQ_1:18;

reconsider B = B as LeftLinearCombination of P by IDEAL_1:42;

set g = Sum B;

reconsider g = Sum B as Polynomial of n,L by POLYNOM1:def 11;

A8: dom A = Seg (k + 1) by A7, FINSEQ_1:def 3;

then k + 1 in dom A by FINSEQ_1:4;

then A9: ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & A /. (k + 1) = m *' p ) by A5;

A10: k <= len A by A7, NAT_1:11;

then ( k <= k + 1 & dom B = Seg k ) by FINSEQ_1:17, NAT_1:11;

then A11: dom B c= dom A by A8, FINSEQ_1:5;

assume A14: for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ; :: thesis: f . b = 0. L

B ^ <*(A /. (k + 1))*> = B ^ <*(A . (k + 1))*> by A8, FINSEQ_1:4, PARTFUN1:def 6

.= A by A7, FINSEQ_3:55 ;

then f = (Sum B) + (Sum <*(A /. (k + 1))*>) by A6, RLVECT_1:41

.= (Sum B) + (A /. (k + 1)) by RLVECT_1:44

.= g + h by POLYNOM1:def 11 ;

then A19: f . b = (g . b) + (h . b) by POLYNOM1:15;

A /. (k + 1) = A . (k + 1) by A8, FINSEQ_1:4, PARTFUN1:def 6;

then A20: 0. L = h . b by A14, A8, A9, FINSEQ_1:4;

len B = k by A10, FINSEQ_1:17;

then g . b = 0. L by A4, A13, A15;

hence f . b = 0. L by A19, A20, RLVECT_1:def 4; :: thesis: verum

end;for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f & f = Sum A & len A = k + 1 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) implies f . b = 0. L )

assume that

A5: A is_MonomialRepresentation_of f and

A6: f = Sum A and

A7: len A = k + 1 ; :: thesis: ( ex i being Element of NAT st

( i in dom A & ex m being Monomial of n,L ex p being Polynomial of n,L st

( A . i = m *' p & p in P & not (m *' p) . b = 0. L ) ) or f . b = 0. L )

set B = A | (Seg k);

reconsider B = A | (Seg k) as FinSequence of (Polynom-Ring (n,L)) by FINSEQ_1:18;

reconsider B = B as LeftLinearCombination of P by IDEAL_1:42;

set g = Sum B;

reconsider g = Sum B as Polynomial of n,L by POLYNOM1:def 11;

A8: dom A = Seg (k + 1) by A7, FINSEQ_1:def 3;

then k + 1 in dom A by FINSEQ_1:4;

then A9: ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & A /. (k + 1) = m *' p ) by A5;

A10: k <= len A by A7, NAT_1:11;

then ( k <= k + 1 & dom B = Seg k ) by FINSEQ_1:17, NAT_1:11;

then A11: dom B c= dom A by A8, FINSEQ_1:5;

now :: thesis: for i being Element of NAT st i in dom B holds

ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & B /. i = m *' p )

then A13:
B is_MonomialRepresentation_of g
;ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & B /. i = m *' p )

let i be Element of NAT ; :: thesis: ( i in dom B implies ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & B /. i = m *' p ) )

assume A12: i in dom B ; :: thesis: ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & B /. i = m *' p )

then B /. i = B . i by PARTFUN1:def 6

.= A . i by A12, FUNCT_1:47

.= A /. i by A11, A12, PARTFUN1:def 6 ;

hence ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & B /. i = m *' p ) by A5, A11, A12; :: thesis: verum

end;( p in P & B /. i = m *' p ) )

assume A12: i in dom B ; :: thesis: ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & B /. i = m *' p )

then B /. i = B . i by PARTFUN1:def 6

.= A . i by A12, FUNCT_1:47

.= A /. i by A11, A12, PARTFUN1:def 6 ;

hence ex m being Monomial of n,L ex p being Polynomial of n,L st

( p in P & B /. i = m *' p ) by A5, A11, A12; :: thesis: verum

assume A14: for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ; :: thesis: f . b = 0. L

A15: now :: thesis: for i being Element of NAT st i in dom B holds

for m being Monomial of n,L

for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L

reconsider h = A /. (k + 1) as Polynomial of n,L by POLYNOM1:def 11;for m being Monomial of n,L

for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L

let i be Element of NAT ; :: thesis: ( i in dom B implies for m being Monomial of n,L

for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L )

assume A16: i in dom B ; :: thesis: for m being Monomial of n,L

for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L

for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L ; :: thesis: verum

end;for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L )

assume A16: i in dom B ; :: thesis: for m being Monomial of n,L

for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L

now :: thesis: for m being Monomial of n,L

for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L

hence
for m being Monomial of n,Lfor p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L

let m be Monomial of n,L; :: thesis: for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L

let p be Polynomial of n,L; :: thesis: ( B . i = m *' p & p in P implies (m *' p) . b = 0. L )

assume that

A17: B . i = m *' p and

A18: p in P ; :: thesis: (m *' p) . b = 0. L

A . i = m *' p by A16, A17, FUNCT_1:47;

hence (m *' p) . b = 0. L by A14, A11, A16, A18; :: thesis: verum

end;(m *' p) . b = 0. L

let p be Polynomial of n,L; :: thesis: ( B . i = m *' p & p in P implies (m *' p) . b = 0. L )

assume that

A17: B . i = m *' p and

A18: p in P ; :: thesis: (m *' p) . b = 0. L

A . i = m *' p by A16, A17, FUNCT_1:47;

hence (m *' p) . b = 0. L by A14, A11, A16, A18; :: thesis: verum

for p being Polynomial of n,L st B . i = m *' p & p in P holds

(m *' p) . b = 0. L ; :: thesis: verum

B ^ <*(A /. (k + 1))*> = B ^ <*(A . (k + 1))*> by A8, FINSEQ_1:4, PARTFUN1:def 6

.= A by A7, FINSEQ_3:55 ;

then f = (Sum B) + (Sum <*(A /. (k + 1))*>) by A6, RLVECT_1:41

.= (Sum B) + (A /. (k + 1)) by RLVECT_1:44

.= g + h by POLYNOM1:def 11 ;

then A19: f . b = (g . b) + (h . b) by POLYNOM1:15;

A /. (k + 1) = A . (k + 1) by A8, FINSEQ_1:4, PARTFUN1:def 6;

then A20: 0. L = h . b by A14, A8, A9, FINSEQ_1:4;

len B = k by A10, FINSEQ_1:17;

then g . b = 0. L by A4, A13, A15;

hence f . b = 0. L by A19, A20, RLVECT_1:def 4; :: thesis: verum

proof

A23:
for k being Nat holds S
let f be Polynomial of n,L; :: thesis: for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = Sum A & len A = 0 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f & f = Sum A & len A = 0 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) implies f . b = 0. L )

assume that

A is_MonomialRepresentation_of f and

A22: ( f = Sum A & len A = 0 ) ; :: thesis: ( ex i being Element of NAT st

( i in dom A & ex m being Monomial of n,L ex p being Polynomial of n,L st

( A . i = m *' p & p in P & not (m *' p) . b = 0. L ) ) or f . b = 0. L )

assume for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ; :: thesis: f . b = 0. L

A = <*> the carrier of (Polynom-Ring (n,L)) by A22;

then f = Sum (<*> the carrier of (Polynom-Ring (n,L))) by A22

.= 0. (Polynom-Ring (n,L)) by RLVECT_1:43

.= 0_ (n,L) by POLYNOM1:def 11 ;

hence f . b = 0. L by POLYNOM1:22; :: thesis: verum

end;for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) holds

f . b = 0. L

let A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f & f = Sum A & len A = 0 & ( for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ) implies f . b = 0. L )

assume that

A is_MonomialRepresentation_of f and

A22: ( f = Sum A & len A = 0 ) ; :: thesis: ( ex i being Element of NAT st

( i in dom A & ex m being Monomial of n,L ex p being Polynomial of n,L st

( A . i = m *' p & p in P & not (m *' p) . b = 0. L ) ) or f . b = 0. L )

assume for i being Element of NAT st i in dom A holds

for m being Monomial of n,L

for p being Polynomial of n,L st A . i = m *' p & p in P holds

(m *' p) . b = 0. L ; :: thesis: f . b = 0. L

A = <*> the carrier of (Polynom-Ring (n,L)) by A22;

then f = Sum (<*> the carrier of (Polynom-Ring (n,L))) by A22

.= 0. (Polynom-Ring (n,L)) by RLVECT_1:43

.= 0_ (n,L) by POLYNOM1:def 11 ;

hence f . b = 0. L by POLYNOM1:22; :: thesis: verum

A24: ex n being Element of NAT st n = len A ;

thus f . b = 0. L by A1, A2, A23, A24; :: thesis: verum