let l, n be Nat; :: thesis: for K being commutative Ring
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 commutative Ring; :: 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) )
A1: len (Line (A,l)) = width A by MATRIX_0:def 7;
assume l in Seg n ; :: thesis: Det (RLine (A,l,(a * (Line (A,l))))) = a * (Det A)
then Det (RLine (A,l,(a * (Line (A,l))))) = a * (Det (RLine (A,l,(Line (A,l))))) by A1, Th34, MATRIX_0:24;
hence Det (RLine (A,l,(a * (Line (A,l))))) = a * (Det A) by Th30; :: thesis: verum