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_{1}[ 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 ;

_{1}[ 0 ]
_{1}[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

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

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_{1}[k] holds

S_{1}[k + 1]

A29:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[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 ) }_{1}[k + 1]
; :: thesis: verum

end;assume A4: S

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

hence
S
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;

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;

( i in dom A & A /. i = m *' p ) } by TARSKI:def 3; :: thesis: verum

end;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 )

then
A9 is_MonomialRepresentation_of g
;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;( 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

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 ) }

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 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 ;

( i in dom A & A /. i = m *' p ) } ; :: thesis: verum

end;( 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 ) } ) )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 ) } ) 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;

end;

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 ) }

( 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;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

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 ) }

( 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;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

( i in dom A & A /. i = m *' p ) } ; :: thesis: verum

( i in dom A & A /. i = m *' p ) } by TARSKI:def 3; :: thesis: verum

proof

for k being Nat holds S
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;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

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