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
for i being Element of NAT st i <= card (Support p) holds
( Support (p | (Upper_Support p,T,i)) = Upper_Support p,T,i & Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i )
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
for i being Element of NAT st i <= card (Support p) holds
( Support (p | (Upper_Support p,T,i)) = Upper_Support p,T,i & Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i )
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
( Support (p | (Upper_Support p,T,i)) = Upper_Support p,T,i & Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i )
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds
( Support (p | (Upper_Support p,T,i)) = Upper_Support p,T,i & Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i )
let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies ( Support (p | (Upper_Support p,T,i)) = Upper_Support p,T,i & Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i ) )
assume A1: i <= card (Support p) ; :: thesis: ( Support (p | (Upper_Support p,T,i)) = Upper_Support p,T,i & Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i )
set u = Upper_Support p,T,i;
set pu = p | (Upper_Support p,T,i);
A2: Support (p | (Upper_Support p,T,i)) = (Support p) /\ (Upper_Support p,T,i) by Th16;
Upper_Support p,T,i c= Support p by A1, Def2;
hence Support (p | (Upper_Support p,T,i)) = Upper_Support p,T,i by A2, XBOOLE_1:28; :: thesis: Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i
set l = Lower_Support p,T,i;
set pl = p | (Lower_Support p,T,i);
Support (p | (Lower_Support p,T,i)) = (Support p) /\ (Lower_Support p,T,i) by Th16;
hence Support (p | (Lower_Support p,T,i)) = Lower_Support p,T,i by XBOOLE_1:28, XBOOLE_1:36; :: thesis: verum