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 :: thesis: for u being object st u in dom (a9 * p) holds
(a9 * p) . u = (0_ (n,L)) . u

let u be object ; :: 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 9
.= 0. L by A2
.= (0_ (n,L)) . u9 by POLYNOM1:22 ;
hence (a9 * p) . u = (0_ (n,L)) . u ; :: thesis: verum

end;

then a9 * p = 0_ (n,L) by A1, FUNCT_1:2;
then for u being object 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 :: thesis: for u being object st u in Support (a * p) holds
u in Support p

let u be object ; :: 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 9;
(a * p) . u9 <> 0. L by A3, POLYNOM1:def 4;
then p . u9 <> 0. L by A4;
hence u in Support p by POLYNOM1:def 4; :: thesis: verum

end;

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

end;

end;