let l, n be Nat; :: thesis: 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)))
let K be commutative Ring; :: 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:92;
then A4: (1_ K) * pK = pK by FVSUM_1:57;
qK is Element of (len pK) -tuples_on the carrier of K by A2, A3, FINSEQ_2:92;
then (1_ K) * qK = qK by FVSUM_1:57;
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))))
.= (Det (RLine (A,l,pK))) + (Det (RLine (A,l,qK))) ;
:: thesis: verum