let R be non degenerated comRing; :: thesis: ([#] (Polynom-Ring (0,R))) /\ ([#] (Polynom-Ring (Polynom-Ring (0,R)))) = {}
set P0 = Polynom-Ring (0,R);
assume ([#] (Polynom-Ring (0,R))) /\ ([#] (Polynom-Ring (Polynom-Ring (0,R)))) <> {} ; :: thesis: contradiction
then consider o being object such that
A2: o in ([#] (Polynom-Ring (0,R))) /\ ([#] (Polynom-Ring (Polynom-Ring (0,R)))) by XBOOLE_0:def 1;
o is Element of [#] (Polynom-Ring (0,R)) by A2, XBOOLE_0:def 4;
then o is not Polynomial of (Polynom-Ring (0,R)) by Th22;
hence contradiction by A2, POLYNOM3:def 10; :: thesis: verum