let V be non empty CLSStruct ; :: thesis: for L1, L2 being C_Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
let L1, L2 be C_Linear_Combination of V; :: thesis: Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier (L1 + L2) or x in (Carrier L1) \/ (Carrier L2) )
assume x in Carrier (L1 + L2) ; :: thesis: x in (Carrier L1) \/ (Carrier L2)
then consider u being VECTOR of V such that
A1: x = u and
A2: (L1 + L2) . u <> 0c ;
(L1 + L2) . u = (L1 . u) + (L2 . u) by Def8;
then ( L1 . u <> 0c or L2 . u <> 0c ) by A2;
then ( x in Carrier L1 or x in Carrier L2 ) by A1;
hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def 3; :: thesis: verum