let K be Ring; :: thesis: for V being VectSp of K
for A being Subset of V
for l1, l2 being Linear_Combination of A st (Carrier l1) /\ (Carrier l2) = {} holds
Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)
let V be VectSp of K; :: thesis: for A being Subset of V
for l1, l2 being Linear_Combination of A st (Carrier l1) /\ (Carrier l2) = {} holds
Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)
let A be Subset of V; :: thesis: for l1, l2 being Linear_Combination of A st (Carrier l1) /\ (Carrier l2) = {} holds
Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)
let l1, l2 be Linear_Combination of A; :: thesis: ( (Carrier l1) /\ (Carrier l2) = {} implies Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2) )
assume A0: (Carrier l1) /\ (Carrier l2) = {} ; :: thesis: Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)
A1: Carrier l1 misses Carrier l2 by A0;
(Carrier l1) \/ (Carrier l2) c= Carrier (l1 + l2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Carrier l1) \/ (Carrier l2) or x in Carrier (l1 + l2) )
assume B1: x in (Carrier l1) \/ (Carrier l2) ; :: thesis: x in Carrier (l1 + l2)
then reconsider x = x as Vector of V ;

per cases ( x in Carrier l1 or x in Carrier l2 ) by B1, XBOOLE_0:def 3;

suppose C1: x in Carrier l1 ; :: thesis: x in Carrier (l1 + l2)

then not x in Carrier l2 by A1, B1, XBOOLE_0:5;
then C2: l2 . x = 0. K ;
(l1 + l2) . x = (l1 . x) + (l2 . x) by VECTSP_6:22
.= l1 . x by C2 ;
then (l1 + l2) . x <> 0. K by C1, VECTSP_6:2;
hence x in Carrier (l1 + l2) ; :: thesis: verum

end;

suppose C1: x in Carrier l2 ; :: thesis: x in Carrier (l1 + l2)

then not x in Carrier l1 by A1, B1, XBOOLE_0:5;
then C2: l1 . x = 0. K ;
(l1 + l2) . x = (l1 . x) + (l2 . x) by VECTSP_6:22
.= l2 . x by C2 ;
then (l1 + l2) . x <> 0. K by C1, VECTSP_6:2;
hence x in Carrier (l1 + l2) ; :: thesis: verum

end;

end;

end;

hence Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2) by VECTSP_6:23; :: thesis: verum