set g = <*1*>;
A1: rng <*1*> = {1} by FINSEQ_1:55;
dom <*1*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then reconsider f = <*1*> as Function of {1},{1} by A1, FUNCT_2:3;
for x, y being set st x in dom f & y in dom f & f . x = f . y holds
x = y

proof

let x, y be set ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume that
A2: x in dom f and
A3: y in dom f and
f . x = f . y ; :: thesis: x = y
x = 1 by A2, TARSKI:def 1;
hence x = y by A3, TARSKI:def 1; :: thesis: verum

end;

then f is one-to-one onto Function of {1},{1} by A1, FUNCT_1:def 8, FUNCT_2:def 3;
hence <*1*> is Permutation of {1} ; :: thesis: verum