let O be Ordinal; :: thesis: for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R
for b being bag of O holds Support (p - (Monom ((p . b),b))) = (Support p) \ {b}
let R be non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of O,R
for b being bag of O holds Support (p - (Monom ((p . b),b))) = (Support p) \ {b}
let p be Polynomial of O,R; :: thesis: for b being bag of O holds Support (p - (Monom ((p . b),b))) = (Support p) \ {b}
let b be bag of O; :: thesis: Support (p - (Monom ((p . b),b))) = (Support p) \ {b}
set M = Monom ((p . b),b);

per cases ( p . b = 0. R or p . b <> 0. R ) ;

suppose A1: p . b = 0. R ; :: thesis: Support (p - (Monom ((p . b),b))) = (Support p) \ {b}

then Monom ((p . b),b) = 0_ (O,R) by Th25;
then A2: p - (Monom ((p . b),b)) = p by POLYRED:4;
not b in Support p by A1, POLYNOM1:def 3;
hence Support (p - (Monom ((p . b),b))) = (Support p) \ {b} by A2, ZFMISC_1:57; :: thesis: verum

end;

suppose p . b <> 0. R ; :: thesis: Support (p - (Monom ((p . b),b))) = (Support p) \ {b}

A3: dom (0_ (O,R)) = Bags O by FUNCT_2:def 1;
A4: ( dom p = Bags O & Bags O = dom (p - (Monom ((p . b),b))) ) by FUNCT_2:def 1;
thus Support (p - (Monom ((p . b),b))) c= (Support p) \ {b} :: according to XBOOLE_0:def 10 :: thesis: (Support p) \ {b} c= Support (p - (Monom ((p . b),b)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support (p - (Monom ((p . b),b))) or x in (Support p) \ {b} )
assume A5: x in Support (p - (Monom ((p . b),b))) ; :: thesis: x in (Support p) \ {b}
then reconsider x = x as bag of O ;
A6: (p - (Monom ((p . b),b))) . x = (p + (- (Monom ((p . b),b)))) . x by POLYNOM1:def 7
.= (p . x) + ((- (Monom ((p . b),b))) . x) by POLYNOM1:15
.= (p . x) + (- ((Monom ((p . b),b)) . x)) by POLYNOM1:17 ;
A7: x <> b

proof

assume x = b ; :: thesis: contradiction
then (Monom ((p . b),b)) . x = p . x by A5, A3, FUNCT_7:31;
then (p . x) - ((Monom ((p . b),b)) . x) = 0. R by RLVECT_1:15;
hence contradiction by A6, A5, POLYNOM1:def 3; :: thesis: verum

end;

(Monom ((p . b),b)) . x = (0_ (O,R)) . x by A7, FUNCT_7:32;
then (Monom ((p . b),b)) . x = 0. R by POLYNOM1:22;
then p . x <> 0. R by A6, A5, POLYNOM1:def 3;
then x in Support p by A4, A5, POLYNOM1:def 3;
hence x in (Support p) \ {b} by A7, ZFMISC_1:56; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Support p) \ {b} or x in Support (p - (Monom ((p . b),b))) )
assume A8: x in (Support p) \ {b} ; :: thesis: x in Support (p - (Monom ((p . b),b)))
then reconsider x = x as bag of O ;
A9: ( x in Support p & x <> b ) by A8, ZFMISC_1:56;
(Monom ((p . b),b)) . x = (0_ (O,R)) . x by A9, FUNCT_7:32;
then A10: (Monom ((p . b),b)) . x = 0. R by POLYNOM1:22;
(p - (Monom ((p . b),b))) . x = (p + (- (Monom ((p . b),b)))) . x by POLYNOM1:def 7
.= (p . x) + ((- (Monom ((p . b),b))) . x) by POLYNOM1:15
.= (p . x) + (- ((Monom ((p . b),b)) . x)) by POLYNOM1:17
.= p . x by A10 ;
then (p - (Monom ((p . b),b))) . x <> 0. R by A9, POLYNOM1:def 3;
hence x in Support (p - (Monom ((p . b),b))) by A8, A4, POLYNOM1:def 3; :: thesis: verum

end;

end;