theorem :: ANPROJ10:51

for X being non empty set
for x being Tuple of 4,X holds
( pi_1324 (pi_1243 x) = pi_1423 x & pi_2143 (pi_1243 x) = pi_2134 x & pi_3412 (pi_1243 x) = pi_4312 x & pi_4321 (pi_1243 x) = pi_3421 x & pi_3412 (pi_1324 x) = pi_2413 x & pi_2143 (pi_1324 x) = pi_3142 x & pi_4321 (pi_1324 x) = pi_4231 x & pi_3412 (pi_1423 x) = pi_2314 x & pi_2143 (pi_1423 x) = pi_4132 x & pi_4321 (pi_1423 x) = pi_3241 x & pi_1243 (pi_1423 x) = pi_1432 x & pi_4321 (pi_1432 x) = pi_2341 x & pi_3412 (pi_1432 x) = pi_3214 x & pi_2143 (pi_1432 x) = pi_4123 x & pi_4321 (pi_3124 x) = pi_4213 x & pi_3412 (pi_3124 x) = pi_2431 x & pi_2143 (pi_3124 x) = pi_1342 x & pi_4312 (pi_3124 x) = pi_4231 x & pi_4321 (pi_3124 x) = pi_4213 x ) ;