let L, L' be C_Linear_Combination of V; :: thesis: ( Carrier L = {} & Carrier L' = {} implies L = L' )
assume A1: ( Carrier L = {} & Carrier L' = {} ) ; :: thesis: L = L'

now

let x be set ; :: thesis: ( x in the carrier of V implies L . x = L' . x )
assume x in the carrier of V ; :: thesis: L . x = L' . x
then reconsider v = x as Element of ;
A2: ( L' . v <> 0c implies v in { u where u is Element of : L' . u <> 0c } ) ;
( L . v <> 0c implies v in { u where u is Element of : L . u <> 0c } ) ;
hence L . x = L' . x by A1, A2; :: thesis: verum

end;

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