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 Def3;
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 ;
hence len P = n by ; :: thesis: verum
end;
hence len P = n ; :: thesis: verum