let R be non degenerated Ring; ([#] (Polynom-Ring R)) \ (rng (canHom R)) <> {}
reconsider p = (0_. R) +* (1,(1. R)) as Polynomial of R ;
assume
([#] (Polynom-Ring R)) \ (rng (canHom R)) = {}
; contradiction
then A2:
[#] (Polynom-Ring R) c= rng (canHom R)
by XBOOLE_1:37;
p in [#] (Polynom-Ring R)
by POLYNOM3:def 10;
then consider x being object such that
A4:
( x in dom (canHom R) & (canHom R) . x = p )
by A2, FUNCT_1:def 3;
reconsider x0 = x as Element of R by A4;
A5: p =
x0 | R
by A4, RING_4:def 6
.=
(0_. R) +* (0,x)
by RING_4:def 5
;
1 in dom (0_. R)
;
then 1. R =
((0_. R) +* (0,x)) . 1
by A5, FUNCT_7:31
.=
(0_. R) . 1
by FUNCT_7:32
.=
0. R
;
hence
contradiction
; verum