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 S1[ 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 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 & 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 ;
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) + () by
.= g + ep by POLYNOM1:def 11 ;
then A12: Support f c= () \/ (Support ep) by POLYNOM1:20;
A13: len A = (len A9) + () by
.= (len A9) + 1 by FINSEQ_1:39 ;
then dom A9 = Seg k by ;
then A14: dom A9 c= dom A by ;
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
.= A9 . i by
.= A9 /. i by ;
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 ;
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 ;
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
.= A9 . i by
.= A9 /. i by ;
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 ; :: 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 ;
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 ;
A27: ( A . (len A) = e & e = Sum <*e*> ) by ;
A28: len A in dom A by ;
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 ;
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 ; :: 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 S1[k + 1] ; :: thesis: verum
end;
A29: S1[ 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 S1[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