let V be RealLinearSpace; :: thesis: for L1, L2 being Linear_Combination of V holds (vector (LC_RLSpace V),L1) + (vector (LC_RLSpace V),L2) = L1 + L2
let L1, L2 be Linear_Combination of V; :: thesis: (vector (LC_RLSpace V),L1) + (vector (LC_RLSpace V),L2) = L1 + L2
set v2 = vector (LC_RLSpace V),L2;
A1: ( L1 = @ (@ L1) & L2 = @ (@ L2) ) ;
L2 in the carrier of (LC_RLSpace V) by Def16;
then A2: L2 in LC_RLSpace V by STRUCT_0:def 5;
L1 in the carrier of (LC_RLSpace V) by Def16;
then L1 in LC_RLSpace V by STRUCT_0:def 5;
hence (vector (LC_RLSpace V),L1) + (vector (LC_RLSpace V),L2) = (LCAdd V) . [L1,(vector (LC_RLSpace V),L2)] by Def1
.= (LCAdd V) . (@ L1),(@ L2) by A2, Def1
.= L1 + L2 by A1, Def19 ;
:: thesis: verum