now :: thesis: for p being object st p in Permutations 0 holds
p in {(<*> NAT)}
let p be object ; :: 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_1:def 12;
q = <*> NAT ;
hence p in {(<*> NAT)} by TARSKI:def 1; :: thesis: verum
end;
then A1: Permutations 0 c= {(<*> NAT)} ;
{(<*> NAT)} c= Permutations 0
proof
let x be object ; :: 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_1:def 12; :: thesis: verum
end;
hence Permutations 0 = {(<*> NAT)} by A1, XBOOLE_0:def 10; :: thesis: verum