theorem :: RLVECT_1:77

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of V
for v1, v2 being Element of V st len F = 2 & v1 = F . 1 & v2 = F . 2 holds
Sum F = v1 + v2