let n be Nat; :: thesis: ex P being non empty permutational set st len P = n
consider p being Permutation of (Seg n);
set P = {p};

now

take n = n; :: thesis: for x being set st x in {p} holds
x is Permutation of (Seg n)
let x be set ; :: thesis: ( x in {p} implies x is Permutation of (Seg n) )
assume x in {p} ; :: thesis: x is Permutation of (Seg n)
hence x is Permutation of (Seg n) by TARSKI:def 1; :: thesis: verum

end;

then reconsider P = {p} as non empty permutational set by Def9;
take P ; :: thesis: len P = n
len P = n

proof

consider x being Element of P;
reconsider y = x as Function of (Seg n),(Seg n) by TARSKI:def 1;
A1: dom y = Seg n by FUNCT_2:67;
then reconsider s = y as FinSequence by FINSEQ_1:def 2;
( n in NAT & len P = len s ) by Def10, ORDINAL1:def 13;
hence len P = n by A1, FINSEQ_1:def 3; :: thesis: verum

end;

hence len P = n ; :: thesis: verum