let n1, n2 be Nat; :: thesis: ( ex s being FinSequence st
( s in P & n1 = len s ) & ex s being FinSequence st
( s in P & n2 = len s ) implies n1 = n2 )
given s1 being FinSequence such that A3: s1 in P and
A4: n1 = len s1 ; :: thesis: ( for s being FinSequence holds
( not s in P or not n2 = len s ) or n1 = n2 )
consider n being Nat such that
A5: for y being set st y in P holds
y is Permutation of (Seg n) by Def3;
s1 is Function of (Seg n),(Seg n) by A3, A5;
then ( n in NAT & dom s1 = Seg n ) by FUNCT_2:52, ORDINAL1:def 12;
then A6: len s1 = n by FINSEQ_1:def 3;
given s2 being FinSequence such that A7: s2 in P and
A8: n2 = len s2 ; :: thesis: n1 = n2
s2 is Permutation of (Seg n) by A7, A5;
then dom s2 = Seg n by FUNCT_2:52;
hence n1 = n2 by A4, A8, A6, FINSEQ_1:def 3; :: thesis: verum