let n be Ordinal; :: thesis:
let T be connected TermOrder of n; :: thesis:
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis:
let f be Polynomial of n,L; :: thesis:
let P be non empty Subset of (Polynom-Ring n,L); :: thesis:
let A be LeftLinearCombination of P; :: thesis:
assume A1: A is_MonomialRepresentation_of f ; :: thesis:
let b be bag of ; :: thesis:
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:
A3: Sum A = f by A1, Def6;
defpred S₁[ Element of 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;
A4: S₁[ 0 ]

proof

let f be Polynomial of n,L; :: thesis:
let A be LeftLinearCombination of P; :: thesis:
assume A5: ( A is_MonomialRepresentation_of f & f = Sum A & len A = 0 ) ; :: thesis:
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 = Sum (<*> the carrier of (Polynom-Ring n,L)) by A5, FINSEQ_1:32
.= 0. (Polynom-Ring n,L) by RLVECT_1:60
.= 0_ n,L by POLYNOM1:def 27 ;
hence f . b = 0. L by POLYNOM1:81; :: thesis:

end;

A6: now

let k be Element of NAT ; :: thesis:
assume A7: S₁[k] ; :: thesis:
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:
let A be LeftLinearCombination of P; :: thesis:
assume A8: ( A is_MonomialRepresentation_of f & f = Sum A & len A = k + 1 ) ; :: thesis:
assume A9: 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:
set B = A | (Seg k);
reconsider B = A | (Seg k) as FinSequence of (Polynom-Ring n,L) by FINSEQ_1:23;
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 27;
A10: dom A = Seg (k + 1) by A8, FINSEQ_1:def 3;
A11: k <= len A by A8, NAT_1:11;
then A12: len B = k by FINSEQ_1:21;
A13: k <= k + 1 by NAT_1:11;
dom B = Seg k by A11, FINSEQ_1:21;
then A14: dom B c= dom A by A10, A13, FINSEQ_1:7;

now

let i be Element of NAT ; :: thesis:
assume A15: i in dom B ; :: thesis:
then consider m being Monomial of n,L, p being Polynomial of n,L such that
A16: ( p in P & A /. i = m *' p ) by A8, A14, Def6;
B /. i = B . i by A15, PARTFUN1:def 8
.= A . i by A15, FUNCT_1:70
.= A /. i by A14, A15, PARTFUN1:def 8 ;
hence ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & B /. i = m *' p ) by A16; :: thesis:

end;

then A17: B is_MonomialRepresentation_of g by Def6;
reconsider h = A /. (k + 1) as Polynomial of n,L by POLYNOM1:def 27;
A18: k + 1 in dom A by A10, FINSEQ_1:6;
B ^ <*(A /. (k + 1))*> = B ^ <*(A . (k + 1))*> by A10, FINSEQ_1:6, PARTFUN1:def 8
.= A by A8, FINSEQ_3:61 ;
then f = (Sum B) + (Sum <*(A /. (k + 1))*>) by A8, RLVECT_1:58
.= (Sum B) + (A /. (k + 1)) by RLVECT_1:61
.= g + h by POLYNOM1:def 27 ;
then A19: f . b = (g . b) + (h . b) by POLYNOM1:def 21;

now

let i be Element of NAT ; :: thesis:
assume A20: i in dom B ; :: thesis:

now

let m be Monomial of n,L; :: thesis:
let p be Polynomial of n,L; :: thesis:
assume A21: ( B . i = m *' p & p in P ) ; :: thesis:
then A . i = m *' p by A20, FUNCT_1:70;
hence (m *' p) . b = 0. L by A9, A14, A20, A21; :: thesis:

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:

end;

then A22: g . b = 0. L by A7, A12, A17;
consider m being Monomial of n,L, p being Polynomial of n,L such that
A23: ( p in P & A /. (k + 1) = m *' p ) by A8, A18, Def6;
A /. (k + 1) = A . (k + 1) by A10, FINSEQ_1:6, PARTFUN1:def 8;
then 0. L = h . b by A9, A10, A23, FINSEQ_1:6;
hence f . b = 0. L by A19, A22, RLVECT_1:def 7; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A24: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A6);
consider n being Element of NAT such that
A25: n = len A ;
thus f . b = 0. L by A1, A2, A3, A24, A25; :: thesis: