for A, B being set
for P being Permutation of A
for Q being Permutation of B holds [:P,Q:] is bijective ;