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

.= 0. V by VECTSP_1:14 ;

:: thesis: verum

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

hence Sum F =
(0. K) * (Sum F)
by X2, RLVECT_2:66
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;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

.= 0. V by VECTSP_1:14 ;

:: thesis: verum