let R be Ring; :: thesis: for X being set holds
( 0_Funcs (X,R) is finite-Support & Support (0_Funcs (X,R)) = {} )
let X be set ; :: thesis: ( 0_Funcs (X,R) is finite-Support & Support (0_Funcs (X,R)) = {} )
Support (0_Funcs (X,R)) = {}

proof

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

end;

hence ( 0_Funcs (X,R) is finite-Support & Support (0_Funcs (X,R)) = {} ) by POLYNOM1:def 5; :: thesis: verum