let n be Nat; :: thesis: permutations (Seg n) = Permutations n

thus permutations (Seg n) c= Permutations n :: according to XBOOLE_0:def 10 :: thesis: Permutations n c= permutations (Seg n)

assume x in Permutations n ; :: thesis: x in permutations (Seg n)

then x is Permutation of (Seg n) by MATRIX_1:def 12;

hence x in permutations (Seg n) ; :: thesis: verum

thus permutations (Seg n) c= Permutations n :: according to XBOOLE_0:def 10 :: thesis: Permutations n c= permutations (Seg n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Permutations n or x in permutations (Seg n) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in permutations (Seg n) or x in Permutations n )

assume x in permutations (Seg n) ; :: thesis: x in Permutations n

then x is Permutation of (Seg n) by Th1;

hence x in Permutations n by MATRIX_1:def 12; :: thesis: verum

end;assume x in permutations (Seg n) ; :: thesis: x in Permutations n

then x is Permutation of (Seg n) by Th1;

hence x in Permutations n by MATRIX_1:def 12; :: thesis: verum

assume x in Permutations n ; :: thesis: x in permutations (Seg n)

then x is Permutation of (Seg n) by MATRIX_1:def 12;

hence x in permutations (Seg n) ; :: thesis: verum