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;
then A2: for x being set st x in Support (Up p,T,(card (Support p))) holds
x in Support p ;
A3: card (Support (Up p,T,(card (Support p)))) = card (Upper_Support p,T,(card (Support p))) by Lm3
.= card (Support p) by Th22 ;

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 A3, CARD_2:67; :: thesis: verum

end;

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

end;

then A5: Support (Up p,T,(card (Support p))) = Support p by A2, TARSKI:2;
A6: dom p = Bags n by FUNCT_2:def 1
.= dom (Up p,T,(card (Support p))) by FUNCT_2:def 1 ;

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 x' = 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 . x' = (Up p,T,(card (Support p))) . x'

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

end;

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

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

end;

end;

end;

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

end;

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