let V be RealLinearSpace; 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; (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 Def14;
then A2:
L2 in LC_RLSpace V
;
L1 in the carrier of (LC_RLSpace V)
by Def14;
then
L1 in LC_RLSpace V
;
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, Def17
;
verum