let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R holds Support (LM p) c= Support p
let n be Ordinal; :: thesis: for p being Polynomial of n,R holds Support (LM p) c= Support p
let p be Polynomial of n,R; :: thesis: Support (LM p) c= Support p

now :: thesis: for o being object st o in Support (LM p) holds
o in Support p

let o be object ; :: thesis: ( o in Support (LM p) implies b₁ in Support p )
assume A: o in Support (LM p) ; :: thesis: b₁ in Support p
then reconsider b = o as Element of Bags n ;
B: (LM p) . b <> 0. R by A, POLYNOM1:def 4;
D: Lt p is Element of Bags n by PRE_POLY:def 12;
C: dom (0_ (n,R)) = Bags n by FUNCT_2:def 1;
E: LM p = (0_ (n,R)) +* ((Lt p),(LC p)) by POLYNOM7:def 4
.= (0_ (n,R)) +* ((Lt p) .--> (LC p)) by C, D, FUNCT_7:def 3 ;

per cases ( b in dom ((Lt p) .--> (LC p)) or not b in dom ((Lt p) .--> (LC p)) ) ;

suppose H: b in dom ((Lt p) .--> (LC p)) ; :: thesis: b₁ in Support p

then I: b = Lt p by TARSKI:def 1;
(LM p) . b = ((Lt p) .--> (LC p)) . b by H, E, FUNCT_4:13
.= LC p by I, FUNCOP_1:72 ;
hence o in Support p by B, I, POLYNOM1:def 4; :: thesis: verum

end;

suppose not b in dom ((Lt p) .--> (LC p)) ; :: thesis: b₁ in Support p

then (LM p) . b = (0_ (n,R)) . b by E, FUNCT_4:11
.= 0. R by POLYNOM1:22 ;
hence o in Support p by A, POLYNOM1:def 4; :: thesis: verum

end;

end;

end;

hence Support (LM p) c= Support p ; :: thesis: verum