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};
{p} is non empty permutational set

proof

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;

hence {p} is non empty permutational set by Def9; :: thesis: verum

end;

then reconsider P = {p} as non empty permutational set ;
A1: len P = n

proof

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

end;

take P ; :: thesis: len P = n
thus len P = n by A1; :: thesis: verum