theorem :: COMPUT_1:87

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