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)

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

hence
Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)
by VECTSP_6:23; :: thesis: verum
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 ;

end;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;

end;