reconsider f = the carrier of V --> 0c as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8;
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
take {} V ; :: thesis: for v being Element of V st not v in {} V holds
f . v = 0
thus for v being Element of V st not v in {} V holds
f . v = 0 by FUNCOP_1:7; :: thesis: verum