let K be Ring; :: thesis: for V being LeftMod of K
for F being FinSequence of V st F = (dom F) --> (0. V) holds
Sum F = 0. V
let V be LeftMod of K; :: thesis: for F being FinSequence of V st F = (dom F) --> (0. V) holds
Sum F = 0. V
let F be FinSequence of V; :: thesis: ( F = (dom F) --> (0. V) implies Sum F = 0. V )
assume AS: F = (dom F) --> (0. V) ; :: thesis: Sum F = 0. V
X2: len F = len F ;
for k being Nat
for v being Element of V st k in dom F & v = F . k holds
F . k = (0. K) * v

proof

let k be Nat; :: thesis: for v being Element of V st k in dom F & v = F . k holds
F . k = (0. K) * v
let v be Element of V; :: thesis: ( k in dom F & v = F . k implies F . k = (0. K) * v )
assume ( k in dom F & v = F . k ) ; :: thesis: F . k = (0. K) * v
hence F . k = 0. V by FUNCOP_1:7, AS
.= (0. K) * v by VECTSP_1:14 ;
:: thesis: verum

end;

hence Sum F = (0. K) * (Sum F) by X2, RLVECT_2:66
.= 0. V by VECTSP_1:14 ;
:: thesis: verum