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

( 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