let F be Field; :: thesis: for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
let V be VectSp of F; :: thesis: for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
let l, m be Linear_Combination of V; :: thesis: ( Carrier l misses Carrier m implies Carrier (l - m) = (Carrier l) \/ (Carrier m) )
assume A1: Carrier l misses Carrier m ; :: thesis: Carrier (l - m) = (Carrier l) \/ (Carrier m)
Carrier (- m) = Carrier m by VECTSP_6:38;
hence Carrier (l - m) = (Carrier l) \/ (Carrier m) by A1, Th31; :: thesis: verum