for n being Nat
for K being Field
for A, B 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 * B)) ) )