reconsider f = the carrier of V --> (0. GF) as Function of the carrier of V,the carrier of GF ;
reconsider f = f as Element of Funcs the carrier of V,the carrier of GF by FUNCT_2:11;
reconsider P = {} V as finite Subset of V ;
take f ; :: thesis: ex T being finite Subset of V st
for v being Element of V st not v in T holds
f . v = 0. GF
take P ; :: thesis: for v being Element of V st not v in P holds
f . v = 0. GF
thus for v being Element of V st not v in P holds
f . v = 0. GF by FUNCOP_1:13; :: thesis: verum