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;
f is Linear_Combination of V

proof

reconsider T = {} V as empty finite Subset of V ;
take T ; :: according to VECTSP_6:def 4 :: thesis: for v being Element of V st not v in T holds
f . v = 0. GF
thus for v being Element of V st not v in T holds
f . v = 0. GF by FUNCOP_1:13; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V ;
take f ; :: thesis: Carrier f = {}
set C = { v where v is Element of V : f . v <> 0. GF } ;

now

assume A1: { v where v is Element of V : f . v <> 0. GF } <> {} ; :: thesis: contradiction
consider x being Element of { v where v is Element of V : f . v <> 0. GF } ;
x in { v where v is Element of V : f . v <> 0. GF } by A1;
then ex v being Element of V st
( x = v & f . v <> 0. GF ) ;
hence contradiction by FUNCOP_1:13; :: thesis: verum

end;

hence Carrier f = {} ; :: thesis: verum