for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being non empty right_complementable Abelian add-associative right_zeroed ModuleStr over R
for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)