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 S1[ 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;
A3: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[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
proof
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;
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 )
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;
then A13: B is_MonomialRepresentation_of g ;
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
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
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
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;
hence 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 ; :: thesis: verum
end;
reconsider h = A /. (k + 1) as Polynomial of n,L by POLYNOM1:def 11;
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;
hence S1[k + 1] ; :: thesis: verum
end;
A21: S1[ 0 ]
proof
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;
A23: for k being Nat holds S1[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