theorem Th7: :: MATRIX14:7

for G being non empty multLoopStr
for x1, x2, y1, y2 being FinSequence of G st len x1 = len x2 & len y1 = len y2 holds
mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2))