let R be Ring; :: thesis: for S being Subring of R
for f being Polynomial of S
for g being Polynomial of R st f = g holds
len f = len g
let S be Subring of R; :: thesis: for f being Polynomial of S
for g being Polynomial of R st f = g holds
len f = len g
let f be Polynomial of S; :: thesis: for g being Polynomial of R st f = g holds
len f = len g
let g be Polynomial of R; :: thesis: ( f = g implies len f = len g )
assume A1: f = g ; :: thesis: len f = len g
A2: len g is_at_least_length_of f

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not len g <= i or f . i = 0. S )
assume i >= len g ; :: thesis: f . i = 0. S
then g . i = 0. R by ALGSEQ_1:8;
hence f . i = 0. S by A1, C0SP1:def 3; :: thesis: verum

end;

for m being Nat st m is_at_least_length_of f holds
len g <= m

proof

let m be Nat; :: thesis: ( m is_at_least_length_of f implies len g <= m )
assume A3: m is_at_least_length_of f ; :: thesis: len g <= m
m is_at_least_length_of g

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not m <= i or g . i = 0. R )
assume i >= m ; :: thesis: g . i = 0. R
then f . i = 0. S by A3;
hence g . i = 0. R by A1, C0SP1:def 3; :: thesis: verum

end;

hence len g <= m by ALGSEQ_1:def 3; :: thesis: verum

end;

hence len f = len g by A2, ALGSEQ_1:def 3; :: thesis: verum