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
( Upper_Support p,T,0 = {} & Lower_Support p,T,0 = Support 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
( Upper_Support p,T,0 = {} & Lower_Support p,T,0 = Support p )
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds
( Upper_Support p,T,0 = {} & Lower_Support p,T,0 = Support p )
let p be Polynomial of n,L; :: thesis: ( Upper_Support p,T,0 = {} & Lower_Support p,T,0 = Support p )
set u = Upper_Support p,T,0 ;
set l = Lower_Support p,T,0 ;
0 <= card (Support p) ;
then card (Upper_Support p,T,0 ) = 0 by Def2;
then Upper_Support p,T,0 , 0 are_equipotent by CARD_1:def 5;
hence Upper_Support p,T,0 = {} by CARD_1:46; :: thesis: Lower_Support p,T,0 = Support p
hence Lower_Support p,T,0 = Support p ; :: thesis: verum