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