let f be C_Linear_Combination of V; :: thesis: ( f = L1 + L2 iff for v being Element of V holds f . v = (L1 . v) + (L2 . v) )
thus ( f = L1 + L2 implies for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) by VALUED_1:1; :: thesis: ( ( for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) implies f = L1 + L2 )
( dom f = the carrier of V & dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:169;
then A1: dom f = (dom L1) /\ (dom L2) ;
assume for v being Element of V holds f . v = (L1 . v) + (L2 . v) ; :: thesis: f = L1 + L2
then for c being set st c in dom f holds
f . c = (L1 . c) + (L2 . c) ;
hence f = L1 + L2 by A1, VALUED_1:def 1; :: thesis: verum