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

for l being Linear_Combination of V

for X being Subset of V st X misses Carrier l holds

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

let V be LeftMod of R; :: thesis: for l being Linear_Combination of V

for X being Subset of V st X misses Carrier l holds

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

let l be Linear_Combination of V; :: thesis: for X being Subset of V st X misses Carrier l holds

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

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

assume A1: X misses Carrier l ; :: thesis: l .: X c= {(0. R)}

set M = l .: X;

for y being object st y in l .: X holds

y in {(0. R)}

for l being Linear_Combination of V

for X being Subset of V st X misses Carrier l holds

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

let V be LeftMod of R; :: thesis: for l being Linear_Combination of V

for X being Subset of V st X misses Carrier l holds

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

let l be Linear_Combination of V; :: thesis: for X being Subset of V st X misses Carrier l holds

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

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

assume A1: X misses Carrier l ; :: thesis: l .: X c= {(0. R)}

set M = l .: X;

for y being object st y in l .: X holds

y in {(0. R)}

proof

hence
l .: X c= {(0. R)}
; :: thesis: verum
let y be object ; :: thesis: ( y in l .: X implies y in {(0. R)} )

assume y in l .: X ; :: thesis: y in {(0. R)}

then consider x being object such that

x in dom l and

A2: x in X and

A3: y = l . x by FUNCT_1:def 6;

reconsider x = x as Element of V by A2;

end;assume y in l .: X ; :: thesis: y in {(0. R)}

then consider x being object such that

x in dom l and

A2: x in X and

A3: y = l . x by FUNCT_1:def 6;

reconsider x = x as Element of V by A2;

now :: thesis: not l . x <> 0. R

hence
y in {(0. R)}
by A3, TARSKI:def 1; :: thesis: verumassume
l . x <> 0. R
; :: thesis: contradiction

then x in Carrier l ;

hence contradiction by A1, A2, XBOOLE_0:def 4; :: thesis: verum

end;then x in Carrier l ;

hence contradiction by A1, A2, XBOOLE_0:def 4; :: thesis: verum