let R be domRing; :: thesis: for f being Element of the carrier of (Polynom-Ring R) holds rng f = (f .: (Support f)) \/ {(0. R)}
let f be Element of the carrier of (Polynom-Ring R); :: thesis: rng f = (f .: (Support f)) \/ {(0. R)}
A1: dom f = NAT by FUNCT_2:def 1;
A2: rng f = f .: (dom f) by RELAT_1:113
.= f .: ((Support f) \/ (NAT \ (Support f))) by A1, XBOOLE_1:45
.= (f .: (Support f)) \/ (f .: (NAT \ (Support f))) by RELAT_1:120 ;
A3: for y being object st y in f .: (NAT \ (Support f)) holds
y in {(0. R)}

proof

let y be object ; :: thesis: ( y in f .: (NAT \ (Support f)) implies y in {(0. R)} )
assume y in f .: (NAT \ (Support f)) ; :: thesis: y in {(0. R)}
then consider x being object such that
A5: ( x in dom f & x in NAT \ (Support f) & y = f . x ) by FUNCT_1:def 6;
f . x = 0. R

proof

assume f . x <> 0. R ; :: thesis: contradiction
then x in Support f by A5, POLYNOM1:def 4;
hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;

hence y in {(0. R)} by TARSKI:def 1, A5; :: thesis: verum

end;

for y being object st y in {(0. R)} holds
y in f .: (NAT \ (Support f))

proof

let y be object ; :: thesis: ( y in {(0. R)} implies y in f .: (NAT \ (Support f)) )
assume A9: y in {(0. R)} ; :: thesis: y in f .: (NAT \ (Support f))
0. R in f .: (NAT \ (Support f))

proof

A10: f . (len f) = 0. R by ALGSEQ_1:8;
then not len f in Support f by POLYNOM1:def 4;
then len f in NAT \ (Support f) by XBOOLE_0:def 5;
hence 0. R in f .: (NAT \ (Support f)) by A10, A1, FUNCT_1:def 6; :: thesis: verum

end;

hence y in f .: (NAT \ (Support f)) by A9, TARSKI:def 1; :: thesis: verum

end;

hence rng f = (f .: (Support f)) \/ {(0. R)} by A2, A3, TARSKI_0:2; :: thesis: verum