theorem Th12: :: MATRIX14:12

for K being Field
for x1, x2, y1, y2 being FinSequence of K st len x1 = len x2 & len y1 = len y2 holds
|((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|