let l, n be Nat; :: thesis: for K being Field
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))
let K be Field; :: thesis: 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))
let pK, qK be FinSequence of K; :: thesis: 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))
let A be Matrix of n,K; :: thesis: ( l in Seg n & len pK = n & len qK = n implies Det (RLine A,l,(pK + qK)) = (Det (RLine A,l,pK)) + (Det (RLine A,l,qK)) )
assume that
A1: l in Seg n and
A2: len pK = n and
A3: len qK = n ; :: thesis: Det (RLine A,l,(pK + qK)) = (Det (RLine A,l,pK)) + (Det (RLine A,l,qK))
pK is Element of (len pK) -tuples_on the carrier of K by FINSEQ_2:110;
then A4: (1_ K) * pK = pK by FVSUM_1:70;
qK is Element of (len pK) -tuples_on the carrier of K by A2, A3, FINSEQ_2:110;
then (1_ K) * qK = qK by FVSUM_1:70;
hence Det (RLine A,l,(pK + qK)) = ((1_ K) * (Det (RLine A,l,pK))) + ((1_ K) * (Det (RLine A,l,qK))) by A1, A2, A3, A4, Th33
.= (Det (RLine A,l,pK)) + ((1_ K) * (Det (RLine A,l,qK))) by VECTSP_1:def 13
.= (Det (RLine A,l,pK)) + (Det (RLine A,l,qK)) by VECTSP_1:def 13 ;
:: thesis: verum