let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R holds (LM p) . (Lt p) = LC p
let n be Ordinal; :: thesis: for p being Polynomial of n,R holds (LM p) . (Lt p) = LC p
let p be Polynomial of n,R; :: thesis: (LM p) . (Lt p) = LC p
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;
B: Lt p in dom ((Lt p) .--> (LC p)) by TARSKI:def 1;
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 ;
hence (LM p) . (Lt p) = ((Lt p) .--> (LC p)) . (Lt p) by B, FUNCT_4:13
.= LC p by FUNCOP_1:72 ;
:: thesis: verum