for n being Nat
for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
for A, B being Matrix of n,K st 0 < n holds
ex P being Function of (Permutations n), the carrier of K st
( Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),P) & ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )