let R be Ring; :: thesis: for V being RightMod of R
for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
let V be RightMod of R; :: thesis: for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
let v be Vector of V; :: thesis: for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
let F, G be FinSequence of V; :: thesis: ( len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) implies Sum F = (Sum G) + v )
( len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) implies Sum F = (Sum G) + v ) by RLVECT_1:38;
hence ( len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) implies Sum F = (Sum G) + v ) by FINSEQ_1:def 3; :: thesis: verum