theorem Th54: :: MATRIX11:54

for n being Nat
for K being commutative Ring
for F being Function of (Seg n),(Seg n)
for A being Matrix of n,K st not F in Permutations n holds
Det (A * F) = 0. K