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

for A being Subset of V

for l being Linear_Combination of A

for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. R)}

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

for l being Linear_Combination of A

for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. R)}

let A be Subset of V; :: thesis: for l being Linear_Combination of A

for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. R)}

let l be Linear_Combination of A; :: thesis: for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. R)}

let X be Subset of V; :: thesis: ( X misses Carrier l & X <> {} implies l .: X = {(0. R)} )

assume that

A1: X misses Carrier l and

A2: X <> {} ; :: thesis: l .: X = {(0. R)}

dom l = [#] V by FUNCT_2:92;

hence l .: X = {(0. R)} by A1, A2, Th28, ZFMISC_1:33; :: thesis: verum

for A being Subset of V

for l being Linear_Combination of A

for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. R)}

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

for l being Linear_Combination of A

for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. R)}

let A be Subset of V; :: thesis: for l being Linear_Combination of A

for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. R)}

let l be Linear_Combination of A; :: thesis: for X being Subset of V st X misses Carrier l & X <> {} holds

l .: X = {(0. R)}

let X be Subset of V; :: thesis: ( X misses Carrier l & X <> {} implies l .: X = {(0. R)} )

assume that

A1: X misses Carrier l and

A2: X <> {} ; :: thesis: l .: X = {(0. R)}

dom l = [#] V by FUNCT_2:92;

hence l .: X = {(0. R)} by A1, A2, Th28, ZFMISC_1:33; :: thesis: verum