let l, n be Nat; :: thesis: for K being Field
for a being Element of K
for pK being FinSequence of K
for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine A,l,(a * pK)) = a * (Det (RLine A,l,pK))
let K be Field; :: thesis: for a being Element of K
for pK being FinSequence of K
for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine A,l,(a * pK)) = a * (Det (RLine A,l,pK))
let a be Element of K; :: thesis: for pK being FinSequence of K
for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine A,l,(a * pK)) = a * (Det (RLine A,l,pK))
let pK be FinSequence of K; :: thesis: for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine A,l,(a * pK)) = a * (Det (RLine A,l,pK))
let A be Matrix of n,K; :: thesis: ( l in Seg n & len pK = n implies Det (RLine A,l,(a * pK)) = a * (Det (RLine A,l,pK)) )
assume A1: ( l in Seg n & len pK = n ) ; :: thesis: Det (RLine A,l,(a * pK)) = a * (Det (RLine A,l,pK))
pK is Element of (len pK) -tuples_on the carrier of K by FINSEQ_2:110;
then ( (a * pK) + ((0. K) * pK) = (a + (0. K)) * pK & a + (0. K) = a ) by FVSUM_1:68, RLVECT_1:10;
hence Det (RLine A,l,(a * pK)) = (a * (Det (RLine A,l,pK))) + ((0. K) * (Det (RLine A,l,pK))) by A1, Th33
.= (a * (Det (RLine A,l,pK))) + (0. K) by VECTSP_1:36
.= a * (Det (RLine A,l,pK)) by RLVECT_1:10 ;
:: thesis: verum