let R be non degenerated Ring; :: thesis: for S being Subring of R
for f being Polynomial of S
for g being monic Polynomial of R st f = g holds
f is monic
let S be Subring of R; :: thesis: for f being Polynomial of S
for g being monic Polynomial of R st f = g holds
f is monic
let f be Polynomial of S; :: thesis: for g being monic Polynomial of R st f = g holds
f is monic
let g be monic Polynomial of R; :: thesis: ( f = g implies f is monic )
assume f = g ; :: thesis: f is monic
hence LC f = LC g by Th9
.= 1. R by RATFUNC1:def 7
.= 1. S by C0SP1:def 3 ;
:: according to RATFUNC1:def 7 :: thesis: verum