let n be Ordinal; :: thesis: for L being 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
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 L be 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
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: for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f 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 P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f 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 A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f implies 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 ) } )
assume A1: A is_MonomialRepresentation_of f ; :: thesis: 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 ) }
defpred S₁[ 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: ex n being Element of NAT st len A = n ;

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
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 ) }

proof

A5: k <= k + 1 by NAT_1:11;
let f be Polynomial of n,L; :: thesis: 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 A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f & len A = k + 1 implies 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 ) } )
assume that
A6: A is_MonomialRepresentation_of f and
A7: len A = k + 1 ; :: thesis: 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 ) }
A8: A <> <*> the carrier of (Polynom-Ring (n,L)) by A7;
A9: Sum A = f by A6;
reconsider A = A as non empty LeftLinearCombination of P by A8;
consider A9 being LeftLinearCombination of P, e being Element of (Polynom-Ring (n,L)) such that
A10: A = A9 ^ <*e*> and
<*e*> is LeftLinearCombination of P by IDEAL_1:33;
A11: dom A = Seg (k + 1) by A7, FINSEQ_1:def 3;
reconsider ep = Sum <*e*> as Polynomial of n,L by POLYNOM1:def 11;
reconsider g = Sum A9 as Polynomial of n,L by POLYNOM1:def 11;
f = (Sum A9) + (Sum <*e*>) by A9, A10, RLVECT_1:41
.= g + ep by POLYNOM1:def 11 ;
then A12: Support f c= (Support g) \/ (Support ep) by POLYNOM1:20;
A13: len A = (len A9) + (len <*e*>) by A10, FINSEQ_1:22
.= (len A9) + 1 by FINSEQ_1:39 ;
then dom A9 = Seg k by A7, FINSEQ_1:def 3;
then A14: dom A9 c= dom A by A11, A5, FINSEQ_1:5;

now :: thesis: for i being Element of NAT st i in dom A9 holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A9 /. i = m *' p )

let i be Element of NAT ; :: thesis: ( i in dom A9 implies ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A9 /. i = m *' p ) )
assume A15: i in dom A9 ; :: thesis: ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A9 /. i = m *' p )
then A /. i = A . i by A14, PARTFUN1:def 6
.= A9 . i by A10, A15, FINSEQ_1:def 7
.= A9 /. i by A15, PARTFUN1:def 6 ;
hence ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A9 /. i = m *' p ) by A6, A14, A15; :: thesis: verum

end;

then A9 is_MonomialRepresentation_of g ;
then A16: 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 A9 & A9 /. i = m *' p ) } by A4, A7, A13;

now :: thesis: for x being object st x in Support f holds
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 ) }

let x be object ; :: thesis: ( x in Support f implies 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 ) } )
assume A17: x in Support f ; :: thesis: 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 ) }
then reconsider u = x as Element of Bags n ;

now :: thesis: ( ( u in Support g & 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 ) } ) or ( u in Support ep & 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 ) } ) )

per cases ( u in Support g or u in Support ep ) by A12, A17, XBOOLE_0:def 3;

case u in Support g ; :: thesis: 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 ) }

then consider Y being set such that
A18: u in Y and
A19: 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 A9 & A9 /. i = m *' p ) } by A16, TARSKI:def 4;
consider m9 being Monomial of n,L, p9 being Polynomial of n,L such that
A20: Y = Support (m9 *' p9) and
A21: ex i being Element of NAT st
( i in dom A9 & A9 /. i = m9 *' p9 ) by A19;
consider i being Element of NAT such that
A22: i in dom A9 and
A23: A9 /. i = m9 *' p9 by A21;
A /. i = A . i by A14, A22, PARTFUN1:def 6
.= A9 . i by A10, A22, FINSEQ_1:def 7
.= A9 /. i by A22, PARTFUN1:def 6 ;
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 A14, A20, A22, A23;
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 A18, TARSKI:def 4; :: thesis: verum

end;

case A24: u in Support ep ; :: thesis: 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 ) }

1 <= len A by A7, NAT_1:11;
then A25: len A in Seg (len A) by FINSEQ_1:1;
dom A = Seg (len A) by FINSEQ_1:def 3;
then A26: ex m9 being Monomial of n,L ex p9 being Polynomial of n,L st
( p9 in P & A /. (len A) = m9 *' p9 ) by A6, A25;
A27: ( A . (len A) = e & e = Sum <*e*> ) by A10, A13, FINSEQ_1:42, RLVECT_1:44;
A28: len A in dom A by A25, FINSEQ_1:def 3;
then A /. (len A) = A . (len A) by PARTFUN1:def 6;
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 A28, A26, A27;
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 A24, TARSKI:def 4; :: thesis: verum

end;

end;

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: verum

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: verum

end;

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

end;

A29: S₁[ 0 ]

proof

let f be Polynomial of n,L; :: thesis: for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & len A = 0 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 A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f & len A = 0 implies 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 ) } )
assume that
A30: A is_MonomialRepresentation_of f and
A31: len A = 0 ; :: thesis: 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 ) }
A = <*> the carrier of (Polynom-Ring (n,L)) by A31;
then Sum A = 0. (Polynom-Ring (n,L)) by RLVECT_1:43;
then f = 0. (Polynom-Ring (n,L)) by A30;
then f = 0_ (n,L) by POLYNOM1:def 11;
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: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A29, A3);
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 A1, A2; :: thesis: verum