let n be Nat; :: thesis: len (Permutations n) = n
consider x being Element of Permutations n;
reconsider q = x as Permutation of (Seg n) by Def11;
A1: dom q = Seg n by FUNCT_2:67;
then reconsider q = q as FinSequence by FINSEQ_1:def 2;
n in NAT by ORDINAL1:def 13;
then len q = n by A1, FINSEQ_1:def 3;
hence len (Permutations n) = n by Def10; :: thesis: verum