let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( Up (p,T,0) = 0_ (n,L) & Low (p,T,0) = p )
let T be connected TermOrder of n; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( Up (p,T,0) = 0_ (n,L) & Low (p,T,0) = p )
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds
( Up (p,T,0) = 0_ (n,L) & Low (p,T,0) = p )
let p be Polynomial of n,L; :: thesis: ( Up (p,T,0) = 0_ (n,L) & Low (p,T,0) = p )
set u = Up (p,T,0);
set l = Low (p,T,0);
A1: 0 <= card (Support p) ;
then Support (Up (p,T,0)) = Upper_Support (p,T,0) by Lm3;
then card (Support (Up (p,T,0))) = 0 by A1, Def2;
then Support (Up (p,T,0)) = {} ;
hence Up (p,T,0) = 0_ (n,L) by POLYNOM7:1; :: thesis: Low (p,T,0) = p
then (0_ (n,L)) + (Low (p,T,0)) = p by A1, Th33;
hence Low (p,T,0) = p by POLYRED:2; :: thesis: verum