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

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 LeftMod of R; :: 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

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 LeftMod of R; :: 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