A1: Permutations 1 c= {(idseq 1)}

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in Permutations 1 or p in {(idseq 1)} )
assume p in Permutations 1 ; :: thesis: p in {(idseq 1)}
then reconsider q = p as Permutation of (Seg 1) by Def11;
A2: ( q is Function of (Seg 1),(Seg 1) & rng q = Seg 1 ) by FUNCT_2:def 3;
A3: dom q = Seg 1 by FUNCT_2:67;
1 in {1} by TARSKI:def 1;
then q . 1 in Seg 1 by A2, FINSEQ_1:4, FUNCT_2:6;
then A4: q . 1 = 1 by FINSEQ_1:4, TARSKI:def 1;
reconsider q = q as FinSequence by A3, FINSEQ_1:def 2;
len q = 1 by A3, FINSEQ_1:def 3;
then q = idseq 1 by A4, FINSEQ_1:57, FINSEQ_2:59;
hence p in {(idseq 1)} by TARSKI:def 1; :: thesis: verum

end;

{(idseq 1)} c= Permutations 1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(idseq 1)} or x in Permutations 1 )
assume x in {(idseq 1)} ; :: thesis: x in Permutations 1
then x = idseq 1 by TARSKI:def 1;
hence x in Permutations 1 by Def11; :: thesis: verum

end;

hence Permutations 1 = {(idseq 1)} by A1, XBOOLE_0:def 10; :: thesis: verum