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 ), 0 are_equipotent by CARD_1:def 5;
then Support (Up p,T,0 ) = {} by CARD_1:46;
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