theorem Th60: :: MATRIX11:60

for n being Nat
for K being commutative Ring
for A, B being Matrix of n,K st 0 < n holds
ex P being Function of (Funcs ((Seg n),(Seg n))), the carrier of K st
( ( for F being Function of (Seg n),(Seg n) ex Path being FinSequence of K st
( len Path = n & ( for Fj, j being Nat st j in Seg n & Fj = F . j holds
Path . j = A * (j,Fj) ) & P . F = ( the multF of K $$ Path) * (Det (B * F)) ) ) & Det (A * B) = the addF of K $$ ((In ((Funcs ((Seg n),(Seg n))),(Fin (Funcs ((Seg n),(Seg n)))))),P) )