let R be Ring; :: thesis: for S being Subring of R
for f being Polynomial of S holds f is Polynomial of R
let S be Subring of R; :: thesis: for f being Polynomial of S holds f is Polynomial of R
let f be Polynomial of S; :: thesis: f is Polynomial of R
the carrier of S c= the carrier of R by C0SP1:def 3;
then reconsider f = f as sequence of R by FUNCT_2:7;
f is finite-Support
proof
consider n being Nat such that
A1: for i being Nat st i >= n holds
f . i = 0. S by ALGSEQ_1:def 1;
take n ; :: according to ALGSEQ_1:def 1 :: thesis: for b1 being set holds
( not n <= b1 or f . b1 = 0. R )
0. S = 0. R by C0SP1:def 3;
hence for b1 being set holds
( not n <= b1 or f . b1 = 0. R ) by A1; :: thesis: verum
end;
hence f is Polynomial of R ; :: thesis: verum