set PR = Polynom-Ring R;
defpred S1[ Element of NAT , object ] means c2 = rpoly (R,(0. R));
A0: for x being Element of NAT ex y being Element of the carrier of (Polynom-Ring R) st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of the carrier of (Polynom-Ring R) st S1[x,y]
take rpoly (x,(0. R)) ; :: thesis: ( rpoly (x,(0. R)) is Element of the carrier of (Polynom-Ring R) & S1[x, rpoly (x,(0. R))] )
thus ( rpoly (x,(0. R)) is Element of the carrier of (Polynom-Ring R) & S1[x, rpoly (x,(0. R))] ) by POLYNOM3:def 10; :: thesis: verum
end;
consider f being Function of NAT, the carrier of (Polynom-Ring R) such that
A1: for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch 3(A0);
 A2: dom f = NAT by FUNCT_2:def 1;
now :: thesis: for x1, x2 being object st x1 in NAT & x2 in NAT & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in NAT & x2 in NAT & f . x1 = f . x2 implies x1 = x2 )
assume A3: ( x1 in NAT & x2 in NAT & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider n = x1, m = x2 as Element of NAT ;
rpoly (n,(0. R)) = f . m by A1, A3
.= rpoly (m,(0. R)) by A1 ;
then n = deg (rpoly (m,(0. R))) by HURWITZ:27
.= m by HURWITZ:27 ;
hence x1 = x2 ; :: thesis: verum
end;
then f is one-to-one by FUNCT_2:19;
then rng f is infinite by A2, CARD_1:59;
hence not Polynom-Ring R is finite ; :: thesis: verum