set x = the Element of 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 = the Element of P 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;

take n ; :: thesis: ex s being FinSequence st

( s in P & n = len s )

take q ; :: thesis: ( q in P & n = len q )

thus ( q in P & n = len q ) by A2, FINSEQ_1:def 3; :: 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 = the Element of P 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;

take n ; :: thesis: ex s being FinSequence st

( s in P & n = len s )

take q ; :: thesis: ( q in P & n = len q )

thus ( q in P & n = len q ) by A2, FINSEQ_1:def 3; :: thesis: verum