theorem Th21: :: BORSUK_7:31

for a, b, c, x, y, z being object st a,b,c are_mutually_distinct holds
product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))}