let l, n be Nat; :: thesis: for K being Field
for a being Element of K
for A being Matrix of n,K st l in Seg n holds
Det (RLine A,l,(a * (Line A,l))) = a * (Det A)
let K be Field; :: thesis: for a being Element of K
for A being Matrix of n,K st l in Seg n holds
Det (RLine A,l,(a * (Line A,l))) = a * (Det A)
let a be Element of K; :: thesis: for A being Matrix of n,K st l in Seg n holds
Det (RLine A,l,(a * (Line A,l))) = a * (Det A)
let A be Matrix of n,K; :: thesis: ( l in Seg n implies Det (RLine A,l,(a * (Line A,l))) = a * (Det A) )
assume A1: l in Seg n ; :: thesis: Det (RLine A,l,(a * (Line A,l))) = a * (Det A)
( len (Line A,l) = width A & width A = n ) by MATRIX_1:25, MATRIX_1:def 8;
then Det (RLine A,l,(a * (Line A,l))) = a * (Det (RLine A,l,(Line A,l))) by A1, Th34;
hence Det (RLine A,l,(a * (Line A,l))) = a * (Det A) by Th30; :: thesis: verum