theorem Th56:
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))))) ) )