theorem Th5: :: MATRIX14:5

for L being non empty addLoopStr
for x1, x2 being FinSequence of L
for i being Nat st len x1 = len x2 & 1 <= i & i <= len x1 holds
( (x1 + x2) . i = (x1 /. i) + (x2 /. i) & (x1 - x2) . i = (x1 /. i) - (x2 /. i) )