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 )
assume for v being Element of V holds f . v = (L1 . v) + (L2 . v) ; :: thesis: f = L1 + L2
then A3: for c being object st c in dom f holds
f . c = (L1 . c) + (L2 . c) ;
( dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:92;
then dom f = (dom L1) /\ (dom L2) by FUNCT_2:92;
hence f = L1 + L2 by A3, VALUED_1:def 1; :: thesis: verum