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;

f is Linear_Combination of V

take f ; :: thesis: Carrier f = {}

set C = { v where v is Element of V : f . v <> 0. GF } ;

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

f is Linear_Combination of V

proof

then reconsider f = f as Linear_Combination of V ;
reconsider T = {} V as empty finite Subset of V ;

take T ; :: according to VECTSP_6:def 1 :: 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:7; :: thesis: verum

end;take T ; :: according to VECTSP_6:def 1 :: 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:7; :: thesis: verum

take f ; :: thesis: Carrier f = {}

set C = { v where v is Element of V : f . v <> 0. GF } ;

now :: thesis: not { v where v is Element of V : f . v <> 0. GF } <> {}

hence
Carrier f = {}
; :: thesis: verumset x = the Element of { v where v is Element of V : f . v <> 0. GF } ;

assume { v where v is Element of V : f . v <> 0. GF } <> {} ; :: thesis: contradiction

then the Element of { v where v is Element of V : f . v <> 0. GF } in { v where v is Element of V : f . v <> 0. GF } ;

then ex v being Element of V st

( the Element of { v where v is Element of V : f . v <> 0. GF } = v & f . v <> 0. GF ) ;

hence contradiction by FUNCOP_1:7; :: thesis: verum

end;assume { v where v is Element of V : f . v <> 0. GF } <> {} ; :: thesis: contradiction

then the Element of { v where v is Element of V : f . v <> 0. GF } in { v where v is Element of V : f . v <> 0. GF } ;

then ex v being Element of V st

( the Element of { v where v is Element of V : f . v <> 0. GF } = v & f . v <> 0. GF ) ;

hence contradiction by FUNCOP_1:7; :: thesis: verum