for n being Nat
for K being Field
for A being Matrix of n,K ex P being Polynomial of K st
( len P = n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) )