let x be Element of P; :: thesis: x is Permutation of Seg (len P)
consider n being Nat such that
A1: for y being set st y in P holds
y is Permutation of Seg n by Def9;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
reconsider q = x as Permutation of Seg n by A1;
A2: dom q = Seg n by FUNCT_2:67;
then reconsider q = q as FinSequence by FINSEQ_1:def 2;
len q = n by A2, FINSEQ_1:def 3;
then Seg (len P) = Seg n by Def10;
hence x is Permutation of Seg (len P) by A1; :: thesis: verum