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

now :: thesis: ex n being Nat st
for x being set st x in { the Permutation of (Seg n)} holds
x is Permutation of (Seg n)

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

end;

then reconsider P = { the Permutation of (Seg n)} as non empty permutational set by Def10;
take P ; :: thesis: len P = n
len P = n

proof

set x = the Element of P;
reconsider y = the Element of P as Function of (Seg n),(Seg n) by TARSKI:def 1;
A1: dom y = Seg n by FUNCT_2:52;
then reconsider s = y as FinSequence by FINSEQ_1:def 2;
( n in NAT & len P = len s ) by Def11, ORDINAL1:def 12;
hence len P = n by A1, FINSEQ_1:def 3; :: thesis: verum

end;

hence len P = n ; :: thesis: verum