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 ;
suppose C1: x in Carrier l1 ; :: thesis: x in Carrier (l1 + l2)
then not x in Carrier l2 by ;
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 ;
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 ;
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 ;
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