let R be non degenerated Ring; :: thesis: for S being Subring of R
for f being non-zero Polynomial of S
for g being Polynomial of R st f = g holds
g is non-zero
let S be Subring of R; :: thesis: for f being non-zero Polynomial of S
for g being Polynomial of R st f = g holds
g is non-zero
let f be non-zero Polynomial of S; :: thesis: for g being Polynomial of R st f = g holds
g is non-zero
let g be Polynomial of R; :: thesis: ( f = g implies g is non-zero )
assume f = g ; :: thesis: g is non-zero
then A1: len f = len g by Th9;
0 < len f by UPROOTS:17;
hence g is non-zero by A1, UPROOTS:17; :: thesis: verum