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