let R be Ring; :: thesis: for X being set holds Support (X --> (0. R)) = {}
let X be set ; :: thesis: Support (X --> (0. R)) = {}
set f = X --> (0. R);
assume Support (X --> (0. R)) <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in Support (X --> (0. R)) by XBOOLE_0:def 1;
A3: x in dom (X --> (0. R)) by A2, POLYNOM1:def 3;
(X --> (0. R)) . x = 0. R by A3, FUNCOP_1:7;
hence contradiction by A2, POLYNOM1:def 3; :: thesis: verum