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