let L, L9 be Linear_Combination of V; :: thesis: ( Carrier L = {} & Carrier L9 = {} implies L = L9 )
assume that
A1: Carrier L = {} and
A2: 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 ;

A3: now :: thesis: not L9 . v <> 0. R

assume L9 . v <> 0. R ; :: thesis: contradiction
then v in { u where u is Vector of V : L9 . u <> 0. R } ;
hence contradiction by A2; :: thesis: verum

end;

now :: thesis: not L . v <> 0. R

assume L . v <> 0. R ; :: thesis: contradiction
then v in { u where u is Vector of V : L . u <> 0. R } ;
hence contradiction by A1; :: thesis: verum

end;

hence L . x = L9 . x by A3; :: thesis: verum

end;

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