theorem :: COMPUT_1:87

for i being Nat holds [!] . <*i*> = i !