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