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: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. GF

take {} V ; :: thesis: for v being Element of V st not v in {} V holds

f . v = 0. GF

thus for v being Element of V st not v in {} V holds

f . v = 0. GF by FUNCOP_1:7; :: thesis: verum

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) 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. GF

take {} V ; :: thesis: for v being Element of V st not v in {} V holds

f . v = 0. GF

thus for v being Element of V st not v in {} V holds

f . v = 0. GF by FUNCOP_1:7; :: thesis: verum