let L, L' be Linear_Combination of V; :: thesis: ( Carrier L = {} & Carrier L' = {} implies L = L' )
reconsider K = L, K' = L' as Function of the carrier of V,the carrier of GF ;
assume that
A2: Carrier L = {} and
A3: Carrier L' = {} ; :: thesis: L = L'

now

let x be set ; :: thesis: ( x in the carrier of V implies K . x = K' . x )
assume x in the carrier of V ; :: thesis: K . x = K' . x
then reconsider v = x as Element of V ;

A4: now

assume L . v <> 0. GF ; :: thesis: contradiction
then v in { u where u is Element of V : L . u <> 0. GF } ;
hence contradiction by A2; :: thesis: verum

end;

now

assume L' . v <> 0. GF ; :: thesis: contradiction
then v in { u where u is Element of V : L' . u <> 0. GF } ;
hence contradiction by A3; :: thesis: verum

end;

hence K . x = K' . x by A4; :: thesis: verum

end;

hence L = L' by FUNCT_2:18; :: thesis: verum