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

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