theorem Th56: :: MATRIX11:56

for n being Nat
for K being commutative Ring
for A, B, C being Matrix of n,K
for i being Nat st i in Seg n holds
ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )