theorem Th36: :: MATRIX11:36

for l, n being Nat
for K being commutative Ring
for pK, qK being FinSequence of K
for A being Matrix of n,K st l in Seg n & len pK = n & len qK = n holds
Det (RLine (A,l,(pK + qK))) = (Det (RLine (A,l,pK))) + (Det (RLine (A,l,qK)))