theorem :: RLVECT_1:78

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