theorem Th33: :: MATRIX11:33

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