A1: rng {} = {} ;
dom {} = {} ;
then reconsider f = {} as Function of {},{} by A1, FUNCT_2:1;
f is one-to-one onto Function of {},{} by A1, FUNCT_2:def 3;
hence {} is Permutation of {} ; :: thesis: verum