let n be Ordinal; :: thesis: for L being non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L holds Support (a * p) c= Support p
let L be non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for a being Element of L holds Support (a * p) c= Support p
let p be Polynomial of n,L; :: thesis: for a being Element of L holds Support (a * p) c= Support p
let a9 be Element of L; :: thesis: Support (a9 * p) c= Support p
A1: dom (0_ n,L) = Bags n by FUNCT_2:def 1
.= dom (a9 * p) by FUNCT_2:def 1 ;

per cases ( a9 = 0. L or a9 <> 0. L ) ;

suppose A2: a9 = 0. L ; :: thesis: Support (a9 * p) c= Support p

now

let u be set ; :: thesis: ( u in dom (a9 * p) implies (a9 * p) . u = (0_ n,L) . u )
assume u in dom (a9 * p) ; :: thesis: (a9 * p) . u = (0_ n,L) . u
then reconsider u9 = u as Element of Bags n ;
(a9 * p) . u9 = a9 * (p . u9) by POLYNOM7:def 10
.= 0. L by A2, VECTSP_1:39
.= (0_ n,L) . u9 by POLYNOM1:81 ;
hence (a9 * p) . u = (0_ n,L) . u ; :: thesis: verum

end;

then a9 * p = 0_ n,L by A1, FUNCT_1:9;
then for u being set st u in Support (a9 * p) holds
u in Support p by POLYNOM7:1;
hence Support (a9 * p) c= Support p by TARSKI:def 3; :: thesis: verum

end;

suppose a9 <> 0. L ; :: thesis: Support (a9 * p) c= Support p

then reconsider a = a9 as non zero Element of L by STRUCT_0:def 12;

now

let u be set ; :: thesis: ( u in Support (a * p) implies u in Support p )
assume A3: u in Support (a * p) ; :: thesis: u in Support p
then reconsider u9 = u as Element of Bags n ;
A4: (a * p) . u9 = a * (p . u9) by POLYNOM7:def 10;
(a * p) . u9 <> 0. L by A3, POLYNOM1:def 9;
then p . u9 <> 0. L by A4, VECTSP_1:36;
hence u in Support p by POLYNOM1:def 9; :: thesis: verum

end;

hence Support (a9 * p) c= Support p by TARSKI:def 3; :: thesis: verum

end;

end;