let n be Nat; :: thesis: len (Permutations n) = n
set x = the Element of Permutations n;
reconsider q = the Element of Permutations n as Permutation of (Seg n) by Def5;
A1: dom q = Seg n by FUNCT_2:52;
then reconsider q = q as FinSequence by FINSEQ_1:def 2;
n in NAT by ORDINAL1:def 12;
then len q = n by A1, FINSEQ_1:def 3;
hence len (Permutations n) = n by Def4; :: thesis: verum