let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds
( Up p,T,(card (Support p)) = p & Low p,T,(card (Support p)) = 0_ n,L )
let T be connected TermOrder of n; :: thesis: for L being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds
( Up p,T,(card (Support p)) = p & Low p,T,(card (Support p)) = 0_ n,L )
let L be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds
( Up p,T,(card (Support p)) = p & Low p,T,(card (Support p)) = 0_ n,L )
let p be Polynomial of n,L; :: thesis: ( Up p,T,(card (Support p)) = p & Low p,T,(card (Support p)) = 0_ n,L )
set u = Up p,T,(card (Support p));
set l = Low p,T,(card (Support p));
Support (Up p,T,(card (Support p))) = (Support p) /\ (Upper_Support p,T,(card (Support p))) by Th16;
then A1: Support (Up p,T,(card (Support p))) c= Support p by XBOOLE_1:17;
A2: card (Support (Up p,T,(card (Support p)))) = card (Upper_Support p,T,(card (Support p))) by Lm3
.= card (Support p) by Th22 ;

A3: now

let x be set ; :: thesis: ( x in Support p implies x in Support (Up p,T,(card (Support p))) )
assume A4: x in Support p ; :: thesis: x in Support (Up p,T,(card (Support p)))

now

assume not x in Support (Up p,T,(card (Support p))) ; :: thesis: contradiction
then Support (Up p,T,(card (Support p))) c< Support p by A1, A4, XBOOLE_0:def 8;
hence contradiction by A2, CARD_2:67; :: thesis: verum

end;

hence x in Support (Up p,T,(card (Support p))) ; :: thesis: verum

end;

for x being set st x in Support (Up p,T,(card (Support p))) holds
x in Support p by A1;
then A5: Support (Up p,T,(card (Support p))) = Support p by A3, TARSKI:2;

A6: now

let x be set ; :: thesis: ( x in dom p implies p . x = (Up p,T,(card (Support p))) . x )
assume x in dom p ; :: thesis: p . x = (Up p,T,(card (Support p))) . x
then reconsider x9 = x as Element of Bags n ;

now

per cases ( x in Support p or not x in Support p ) ;

case x in Support p ; :: thesis: p . x9 = (Up p,T,(card (Support p))) . x9

hence p . x9 = (Up p,T,(card (Support p))) . x9 by A5, Th16; :: thesis: verum

end;

case A7: not x in Support p ; :: thesis: p . x9 = (Up p,T,(card (Support p))) . x9

hence p . x9 = 0. L by POLYNOM1:def 9
.= (Up p,T,(card (Support p))) . x9 by A5, A7, POLYNOM1:def 9 ;
:: thesis: verum

end;

end;

end;

hence p . x = (Up p,T,(card (Support p))) . x ; :: thesis: verum

end;

dom p = Bags n by FUNCT_2:def 1
.= dom (Up p,T,(card (Support p))) by FUNCT_2:def 1 ;
hence A8: p = Up p,T,(card (Support p)) by A6, FUNCT_1:9; :: thesis: Low p,T,(card (Support p)) = 0_ n,L
thus 0_ n,L = p + (- p) by POLYRED:3
.= ((Low p,T,(card (Support p))) + p) + (- p) by A8, Th33
.= (Low p,T,(card (Support p))) + (p + (- p)) by POLYNOM1:80
.= (Low p,T,(card (Support p))) + (0_ n,L) by POLYRED:3
.= Low p,T,(card (Support p)) by POLYRED:2 ; :: thesis: verum