theorem Th18: :: HILB10_7:18

for a, b being object
for f, g being FinSequence holds Swap ((f ^ g),a,b) = (Swap (f,a,b)) ^ (Swap (g,a,b))