now

let p be set ; :: thesis: ( p in Permutations 0 implies p in {(<*> NAT )} )
assume p in Permutations 0 ; :: thesis: p in {(<*> NAT )}
then reconsider q = p as Permutation of (Seg 0 ) by MATRIX_2:def 11;
q = <*> NAT ;
hence p in {(<*> NAT )} by TARSKI:def 1; :: thesis: verum

end;

then A1: Permutations 0 c= {(<*> NAT )} by TARSKI:def 3;
{(<*> NAT )} c= Permutations 0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(<*> NAT )} or x in Permutations 0 )
assume x in {(<*> NAT )} ; :: thesis: x in Permutations 0
then x is Permutation of (Seg 0 ) by Lm4, TARSKI:def 1;
hence x in Permutations 0 by MATRIX_2:def 11; :: thesis: verum

end;

hence Permutations 0 = {(<*> NAT )} by A1, XBOOLE_0:def 10; :: thesis: verum