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

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