for K being Ring
for n being Nat st n >= 1 holds
Det (1. (K,n)) = 1_ K