set a = I --> (1_ G);
take I --> (1_ G) ; :: thesis: I --> (1_ G) is finite-support
support (I --> (1_ G)) = {}
proof
assume support (I --> (1_ G)) <> {} ; :: thesis: contradiction
then consider x being object such that
A1: x in support (I --> (1_ G)) by XBOOLE_0:def 1;
( (I --> (1_ G)) . x <> 1_ G & x in I ) by A1, Def2;
hence contradiction by FUNCOP_1:7; :: thesis: verum
end;
hence I --> (1_ G) is finite-support ; :: thesis: verum