let R be Ring; :: thesis: for V being LeftMod of R

for A being Subset of V

for l1, l2 being Linear_Combination of A st Carrier l1 misses Carrier l2 holds

Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

let V be LeftMod of R; :: thesis: for A being Subset of V

for l1, l2 being Linear_Combination of A st Carrier l1 misses 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 misses Carrier l2 holds

Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

let l1, l2 be Linear_Combination of A; :: thesis: ( Carrier l1 misses Carrier l2 implies Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2) )

assume A1: Carrier l1 misses Carrier l2 ; :: thesis: Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

A2: Carrier l1 misses Carrier (- l2) by A1, VECTSP_6:38;

thus Carrier (l1 - l2) = Carrier (l1 + (- l2))

.= (Carrier l1) \/ (Carrier (- l2)) by A2, Th31

.= (Carrier l1) \/ (Carrier l2) by VECTSP_6:38 ; :: thesis: verum

for A being Subset of V

for l1, l2 being Linear_Combination of A st Carrier l1 misses Carrier l2 holds

Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

let V be LeftMod of R; :: thesis: for A being Subset of V

for l1, l2 being Linear_Combination of A st Carrier l1 misses 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 misses Carrier l2 holds

Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

let l1, l2 be Linear_Combination of A; :: thesis: ( Carrier l1 misses Carrier l2 implies Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2) )

assume A1: Carrier l1 misses Carrier l2 ; :: thesis: Carrier (l1 - l2) = (Carrier l1) \/ (Carrier l2)

A2: Carrier l1 misses Carrier (- l2) by A1, VECTSP_6:38;

thus Carrier (l1 - l2) = Carrier (l1 + (- l2))

.= (Carrier l1) \/ (Carrier (- l2)) by A2, Th31

.= (Carrier l1) \/ (Carrier l2) by VECTSP_6:38 ; :: thesis: verum