let V be Z_Module; :: thesis: for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. INT.Ring)}
let l be Linear_Combination of V; :: thesis: for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. INT.Ring)}
let X be Subset of V; :: thesis: ( X misses Carrier l implies l .: X c= {(0. INT.Ring)} )
assume A1: X misses Carrier l ; :: thesis: l .: X c= {(0. INT.Ring)}
set M = l .: X;
for y being object st y in l .: X holds
y in {(0. INT.Ring)}

proof

let y be object ; :: thesis: ( y in l .: X implies y in {(0. INT.Ring)} )
assume y in l .: X ; :: thesis: y in {(0. INT.Ring)}
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. INT.Ring

assume l . x <> 0. INT.Ring ; :: thesis: contradiction
then x in Carrier l ;
hence contradiction by A1, A2, XBOOLE_0:def 4; :: thesis: verum

end;

hence y in {(0. INT.Ring)} by A3, TARSKI:def 1; :: thesis: verum

end;

hence l .: X c= {(0. INT.Ring)} ; :: thesis: verum