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

per cases ;

suppose A2: a9 = 0. L ; :: thesis:

now :: thesis:

let u be object ; :: thesis:
assume u in dom (a9 * p) ; :: thesis:
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:

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:

end;

suppose a9 <> 0. L ; :: thesis:

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

now :: thesis:

let u be object ; :: thesis:
assume A3: u in Support (a * p) ; :: thesis:
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:

end;

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

end;

end;