for X being non empty set
for x being Tuple of 4,X holds
( pi_1342 x = pi_34 (pi_23 x) & pi_1423 x = pi_34 (pi_24 x) & pi_2143 x = pi_12 (pi_34 x) & pi_2314 x = pi_23 (pi_12 x) & pi_2341 x = pi_34 (pi_23 (pi_12 x)) & pi_2413 x = pi_34 (pi_24 (pi_12 x)) & pi_2431 x = pi_24 (pi_12 x) & pi_3124 x = pi_23 (pi_13 x) & pi_3142 x = pi_24 (pi_34 (pi_13 x)) & pi_3241 x = pi_34 (pi_13 x) & pi_3412 x = pi_24 (pi_13 x) & pi_3421 x = pi_24 (pi_23 (pi_13 x)) & pi_4123 x = pi_23 (pi_34 (pi_14 x)) & pi_4132 x = pi_24 (pi_14 x) & pi_4213 x = pi_34 (pi_14 x) & pi_4312 x = pi_23 (pi_24 (pi_14 x)) & pi_4321 x = pi_23 (pi_14 x) ) ;