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 a' be Element of L; :: thesis: Support (a' * p) c= Support p
A1: dom (0_ n,L) = Bags n by FUNCT_2:def 1
.= dom (a' * p) by FUNCT_2:def 1 ;

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

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

now

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

end;

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

end;

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

then reconsider a = a' as non zero Element of L by STRUCT_0:def 15;

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 u' = u as Element of Bags n ;
A4: (a * p) . u' <> 0. L by A3, POLYNOM1:def 9;
(a * p) . u' = a * (p . u') by POLYNOM7:def 10;
then p . u' <> 0. L by A4, VECTSP_1:36;
hence u in Support p by POLYNOM1:def 9; :: thesis: verum

end;

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

end;

end;