for a, b, c, x, y, z being object
for X, Y, Z being set st a,b,c are_mutually_distinct & x in X & y in Y & z in Z holds
(a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z))