set g = <*1*>;
A1:
rng <*1*> = {1}
by FINSEQ_1:38;
dom <*1*> = {1}
by FINSEQ_1:2, FINSEQ_1:38;
then reconsider f = <*1*> as Function of {1},{1} by A1, FUNCT_2:1;
f is one-to-one onto Function of {1},{1}
by A1, FUNCT_2:def 3;
hence
<*1*> is Permutation of {1}
; verum