let f be 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 A3: for v being Element of V holds f . v = (L1 . v) + (L2 . v) ; :: thesis: f = L1 + L2
thus f = L1 + L2 :: thesis: verum

proof

let v be Element of the carrier of V; :: according to FUNCT_2:def 8 :: thesis: f . v = (L1 + L2) . v
thus f . v = (L1 . v) + (L2 . v) by A3
.= (L1 + L2) . v by VALUED_1:1 ; :: thesis: verum

end;