let n be Ordinal; :: 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:
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 & len A = $1 holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } ;
A2: S₁[ 0 ]

let f be Polynomial of n,L; :: thesis:
let A be LeftLinearCombination of P; :: thesis:
assume A3: ( A is_MonomialRepresentation_of f & len A = 0 ) ; :: thesis:
then A = <*> the carrier of (Polynom-Ring n,L) by FINSEQ_1:32;
then Sum A = 0. (Polynom-Ring n,L) by RLVECT_1:60;
then f = 0. (Polynom-Ring n,L) by A3, Def6;
then f = 0_ n,L by POLYNOM1:def 27;
then Support f = {} by POLYNOM7:1;
hence Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } by XBOOLE_1:2; :: thesis:

end;

A4: now

let k be Element of NAT ; :: thesis:
assume A5: S₁[k] ; :: thesis:
for f being Polynomial of n,L
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & len A = k + 1 holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }

let f be Polynomial of n,L; :: thesis:
let A be LeftLinearCombination of P; :: thesis:
assume A6: ( A is_MonomialRepresentation_of f & len A = k + 1 ) ; :: thesis:
then A7: ( Sum A = f & ( for i being Element of NAT st i in dom A holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A /. i = m *' p ) ) ) by Def6;
A <> <*> the carrier of (Polynom-Ring n,L) by A6, FINSEQ_1:32;
then reconsider A = A as non empty LeftLinearCombination of P ;
consider A' being LeftLinearCombination of P, e being Element of (Polynom-Ring n,L) such that
A8: ( A = A' ^ <*e*> & <*e*> is LeftLinearCombination of P ) by IDEAL_1:33;
A9: len A = (len A') + (len <*e*>) by A8, FINSEQ_1:35
.= (len A') + 1 by FINSEQ_1:56 ;
reconsider g = Sum A' as Polynomial of n,L by POLYNOM1:def 27;
A10: dom A = Seg (k + 1) by A6, FINSEQ_1:def 3;
A11: dom A' = Seg k by A6, A9, FINSEQ_1:def 3;
k <= k + 1 by NAT_1:11;
then A12: dom A' c= dom A by A10, A11, FINSEQ_1:7;

let i be Element of NAT ; :: thesis:
assume A13: i in dom A' ; :: thesis:
then A /. i = A . i by A12, PARTFUN1:def 8
.= A' . i by A8, A13, FINSEQ_1:def 7
.= A' /. i by A13, PARTFUN1:def 8 ;
hence ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A' /. i = m *' p ) by A6, A12, A13, Def6; :: thesis:

end;

then A' is_MonomialRepresentation_of g by Def6;
then A14: Support g c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A' & A' /. i = m *' p ) } by A5, A6, A9;
reconsider ep = Sum <*e*> as Polynomial of n,L by POLYNOM1:def 27;
f = (Sum A') + (Sum <*e*>) by A7, A8, RLVECT_1:58
.= g + ep by POLYNOM1:def 27 ;
then A15: Support f c= (Support g) \/ (Support ep) by POLYNOM1:79;

let x be set ; :: thesis:
assume A16: x in Support f ; :: thesis:
then reconsider u = x as Element of Bags n ;

per cases by A15, A16, XBOOLE_0:def 3;

case u in Support g ; :: thesis:

then consider Y being set such that
A17: ( u in Y & Y in { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A' & A' /. i = m *' p ) } ) by A14, TARSKI:def 4;
consider m' being Monomial of n,L, p' being Polynomial of n,L such that
A18: ( Y = Support (m' *' p') & ex i being Element of NAT st
( i in dom A' & A' /. i = m' *' p' ) ) by A17;
consider i being Element of NAT such that
A19: ( i in dom A' & A' /. i = m' *' p' ) by A18;
A /. i = A . i by A12, A19, PARTFUN1:def 8
.= A' . i by A8, A19, FINSEQ_1:def 7
.= A' /. i by A19, PARTFUN1:def 8 ;
then Y in { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } by A12, A18, A19;
hence u in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } by A17, TARSKI:def 4; :: thesis:

end;

case A20: u in Support ep ; :: thesis:

A21: A . (len A) = e by A8, A9, FINSEQ_1:59;
A22: dom A = Seg (len A) by FINSEQ_1:def 3;
1 <= len A by A6, NAT_1:11;
then A23: len A in Seg (len A) by FINSEQ_1:3;
then A24: len A in dom A by FINSEQ_1:def 3;
A25: ex m' being Monomial of n,L ex p' being Polynomial of n,L st
( p' in P & A /. (len A) = m' *' p' ) by A6, A22, A23, Def6;
A26: A /. (len A) = A . (len A) by A24, PARTFUN1:def 8;
e = Sum <*e*> by RLVECT_1:61;
then Support ep in { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } by A21, A24, A25, A26;
hence u in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } by A20, TARSKI:def 4; :: thesis:

end;

hence x in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } ; :: thesis:

end;

hence Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } by TARSKI:def 3; :: thesis:

end;

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

end;

A27: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A4);
consider n being Element of NAT such that
A28: len A = n ;
thus Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } by A1, A27, A28; :: thesis: