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 :: thesis: for x being object st x in Support p holds
x in Support (Up (p,T,(card (Support p))))

let x be object ; :: 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 :: thesis: x in Support (Up (p,T,(card (Support p))))

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:48; :: thesis: verum

end;

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

end;

for x being object 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 :: thesis: for x being object st x in dom p holds
p . x = (Up (p,T,(card (Support p)))) . x

let x be object ; :: 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 :: thesis: ( ( x in Support p & p . x9 = (Up (p,T,(card (Support p)))) . x9 ) or ( not x in Support p & p . x9 = (Up (p,T,(card (Support p)))) . x9 ) )

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 4
.= (Up (p,T,(card (Support p)))) . x9 by A5, A7, POLYNOM1:def 4 ;
:: 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:2; :: 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:21
.= (Low (p,T,(card (Support p)))) + (0_ (n,L)) by POLYRED:3
.= Low (p,T,(card (Support p))) by POLYRED:2 ; :: thesis: verum