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) ) )

set u = Upper_Support (p,T,i);

set pu = p | (Upper_Support (p,T,i));

set l = Lower_Support (p,T,i);

set pl = p | (Lower_Support (p,T,i));

assume 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) )

then A1: Upper_Support (p,T,i) c= Support p by Def2;

Support (p | (Upper_Support (p,T,i))) = (Support p) /\ (Upper_Support (p,T,i)) by Th16;

hence Support (p | (Upper_Support (p,T,i))) = Upper_Support (p,T,i) by A1, XBOOLE_1:28; :: thesis: Support (p | (Lower_Support (p,T,i))) = 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

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) ) )

set u = Upper_Support (p,T,i);

set pu = p | (Upper_Support (p,T,i));

set l = Lower_Support (p,T,i);

set pl = p | (Lower_Support (p,T,i));

assume 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) )

then A1: Upper_Support (p,T,i) c= Support p by Def2;

Support (p | (Upper_Support (p,T,i))) = (Support p) /\ (Upper_Support (p,T,i)) by Th16;

hence Support (p | (Upper_Support (p,T,i))) = Upper_Support (p,T,i) by A1, XBOOLE_1:28; :: thesis: Support (p | (Lower_Support (p,T,i))) = 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