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

now :: thesis: for x being object st x in the carrier of V holds
L . x = L9 . x

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

end;

hence L = L9 by FUNCT_2:12; :: thesis: verum