let n be Nat; :: thesis: ex P being non empty permutational set st len P = n

set p = the Permutation of (Seg n);

set P = { the Permutation of (Seg n)};

take P ; :: thesis: len P = n

len P = n

set p = the Permutation of (Seg n);

set P = { the Permutation of (Seg n)};

now :: thesis: ex n being Nat st

for x being set st x in { the Permutation of (Seg n)} holds

x is Permutation of (Seg n)

then reconsider P = { the Permutation of (Seg n)} as non empty permutational set by Def3;for x being set st x in { the Permutation of (Seg n)} holds

x is Permutation of (Seg n)

take n = n; :: thesis: for x being set st x in { the Permutation of (Seg n)} holds

x is Permutation of (Seg n)

let x be set ; :: thesis: ( x in { the Permutation of (Seg n)} implies x is Permutation of (Seg n) )

assume x in { the Permutation of (Seg n)} ; :: thesis: x is Permutation of (Seg n)

hence x is Permutation of (Seg n) by TARSKI:def 1; :: thesis: verum

end;x is Permutation of (Seg n)

let x be set ; :: thesis: ( x in { the Permutation of (Seg n)} implies x is Permutation of (Seg n) )

assume x in { the Permutation of (Seg n)} ; :: thesis: x is Permutation of (Seg n)

hence x is Permutation of (Seg n) by TARSKI:def 1; :: thesis: verum

take P ; :: thesis: len P = n

len P = n

proof

hence
len P = n
; :: thesis: verum
set x = the Element of P;

reconsider y = the Element of P as Function of (Seg n),(Seg n) by TARSKI:def 1;

A1: dom y = Seg n by FUNCT_2:52;

then reconsider s = y as FinSequence by FINSEQ_1:def 2;

( n in NAT & len P = len s ) by Def4, ORDINAL1:def 12;

hence len P = n by A1, FINSEQ_1:def 3; :: thesis: verum

end;reconsider y = the Element of P as Function of (Seg n),(Seg n) by TARSKI:def 1;

A1: dom y = Seg n by FUNCT_2:52;

then reconsider s = y as FinSequence by FINSEQ_1:def 2;

( n in NAT & len P = len s ) by Def4, ORDINAL1:def 12;

hence len P = n by A1, FINSEQ_1:def 3; :: thesis: verum