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 A1: ( l in Seg n & len pK = n & len qK = n ) ; :: thesis: Det (RLine A,l,(pK + qK)) = (Det (RLine A,l,pK)) + (Det (RLine A,l,qK))
then ( pK is Element of (len pK) -tuples_on the carrier of K & qK is Element of (len pK) -tuples_on the carrier of K ) by FINSEQ_2:110;
then ( (1_ K) * pK = pK & (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, 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