for X being Group-Sequence
for x, y, z being Element of (product X)
for x1, y1, z1 being FinSequence st x = x1 & y = y1 & z = z1 holds
( z = x + y iff for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) )