for K being Field
for i being Element of NAT holds 1. (K,<*i*>) = <*(1. (K,i))*>