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