for i being Element of NAT holds [!] . <*i*> = i !