let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

let L1, L2 be 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 Element of V such that

A1: x = u and

A2: (L1 + L2) . u <> 0. GF ;

(L1 + L2) . u = (L1 . u) + (L2 . u) by Th22;

then ( L1 . u <> 0. GF or L2 . u <> 0. GF ) by A2, RLVECT_1:4;

then ( x in { v1 where v1 is Element of V : L1 . v1 <> 0. GF } or x in { v2 where v2 is Element of V : L2 . v2 <> 0. GF } ) by A1;

hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def 3; :: thesis: verum

for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

let L1, L2 be 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 Element of V such that

A1: x = u and

A2: (L1 + L2) . u <> 0. GF ;

(L1 + L2) . u = (L1 . u) + (L2 . u) by Th22;

then ( L1 . u <> 0. GF or L2 . u <> 0. GF ) by A2, RLVECT_1:4;

then ( x in { v1 where v1 is Element of V : L1 . v1 <> 0. GF } or x in { v2 where v2 is Element of V : L2 . v2 <> 0. GF } ) by A1;

hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def 3; :: thesis: verum