let n be Ordinal; 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
for i being Element of NAT st i <= card (Support p) holds
( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p )
let T be connected TermOrder of n; for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p )
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p )
let p be Polynomial of n,L; for i being Element of NAT st i <= card (Support p) holds
( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p )
let i be Element of NAT ; ( i <= card (Support p) implies ( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p ) )
assume A1:
i <= card (Support p)
; ( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p )
then
( Support (p | (Upper_Support (p,T,i))) = Upper_Support (p,T,i) & Support (p | (Lower_Support (p,T,i))) = Lower_Support (p,T,i) )
by Lm3;
hence
( Support (Up (p,T,i)) c= Support p & Support (Low (p,T,i)) c= Support p )
by A1, Def2, Th24; verum