let F be Field; :: thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let V be VectSp of F; :: thesis: for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let l be Linear_Combination of V; :: thesis: for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let X be Subset of V; :: thesis: ( X misses Carrier l & X <> {} implies l .: X = {(0. F)} )
assume that
A1: X misses Carrier l and
A2: X <> {} ; :: thesis: l .: X = {(0. F)}
dom l = [#] V by FUNCT_2:92;
then A3: l .: X <> {} by A2, RELAT_1:119;
l .: X c= {(0. F)} by A1, Th28;
hence l .: X = {(0. F)} by A3, ZFMISC_1:33; :: thesis: verum