let l, n be Nat; :: thesis: for K being commutative Ring
for pK being FinSequence of K
for a being Element 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 commutative Ring; :: thesis: for pK being FinSequence of K
for a being Element 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 Element 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 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 that
A1: l in Seg n and
A2: 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:92;
then A3: (a * pK) + ((0. K) * pK) = (a + (0. K)) * pK by FVSUM_1:55;
a + (0. K) = a by RLVECT_1:4;
hence Det (RLine (A,l,(a * pK))) = (a * (Det (RLine (A,l,pK)))) + ((0. K) * (Det (RLine (A,l,pK)))) by A1, A2, A3, Th33
.= a * (Det (RLine (A,l,pK))) by RLVECT_1:4 ;
:: thesis: verum