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 Def10;
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