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

proof

{(idseq 1)} c= Permutations 1
let p be object ; :: 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 Def5;

A2: dom q = Seg 1 by FUNCT_2:52;

( rng q = Seg 1 & 1 in {1} ) by FUNCT_2:def 3, TARSKI:def 1;

then q . 1 in Seg 1 by FINSEQ_1:2, FUNCT_2:4;

then A3: q . 1 = 1 by FINSEQ_1:2, TARSKI:def 1;

reconsider q = q as FinSequence by A2, FINSEQ_1:def 2;

len q = 1 by A2, FINSEQ_1:def 3;

then q = idseq 1 by A3, FINSEQ_1:40, FINSEQ_2:50;

hence p in {(idseq 1)} by TARSKI:def 1; :: thesis: verum

end;assume p in Permutations 1 ; :: thesis: p in {(idseq 1)}

then reconsider q = p as Permutation of (Seg 1) by Def5;

A2: dom q = Seg 1 by FUNCT_2:52;

( rng q = Seg 1 & 1 in {1} ) by FUNCT_2:def 3, TARSKI:def 1;

then q . 1 in Seg 1 by FINSEQ_1:2, FUNCT_2:4;

then A3: q . 1 = 1 by FINSEQ_1:2, TARSKI:def 1;

reconsider q = q as FinSequence by A2, FINSEQ_1:def 2;

len q = 1 by A2, FINSEQ_1:def 3;

then q = idseq 1 by A3, FINSEQ_1:40, FINSEQ_2:50;

hence p in {(idseq 1)} by TARSKI:def 1; :: thesis: verum

proof

hence
Permutations 1 = {(idseq 1)}
by A1, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: 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 Def5; :: thesis: verum

end;assume x in {(idseq 1)} ; :: thesis: x in Permutations 1

then x = idseq 1 by TARSKI:def 1;

hence x in Permutations 1 by Def5; :: thesis: verum