let R be Ring; :: thesis: for V being LeftMod of R
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. R
let V be LeftMod of R; :: thesis: for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. R
let l be Linear_Combination of V; :: thesis: for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. R
let A be Subset of V; :: thesis: for v being Element of V st not v in A holds
(l ! A) . v = 0. R
let v be Element of V; :: thesis: ( not v in A implies (l ! A) . v = 0. R )
assume not v in A ; :: thesis: (l ! A) . v = 0. R
then A1: v in A ` by XBOOLE_0:def 5;
A2: dom (l ! A) = [#] V by FUNCT_2:92;
( dom ((A `) --> (0. R)) = A ` & dom (l ! A) = (dom (l | A)) \/ (dom ((A `) --> (0. R))) ) by FUNCT_4:def 1;
then (l ! A) . v = ((A `) --> (0. R)) . v by A1, A2, FUNCT_4:def 1
.= 0. R by A1, FUNCOP_1:7 ;
hence (l ! A) . v = 0. R ; :: thesis: verum