for K being Field
for n being Nat holds ((1. (K,n)) @) ~ = 1. (K,n)