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 Def3;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider q = x as Permutation of (Seg n) by A1;
A2: dom q = Seg n by FUNCT_2:52;
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 Def4;
hence x is Permutation of (Seg (len P)) by A1; :: thesis: verum