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

proof

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 Def12;
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;

{(idseq 1)} c= Permutations 1

proof

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 Def12; :: thesis: verum

end;

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