let n be Nat; :: thesis: for K being Field
for a being Element of K
for A being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine A,i,(a * (Line A,j))) = 0. K
let K be Field; :: thesis: for a being Element of K
for A being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine A,i,(a * (Line A,j))) = 0. K
let a be Element of K; :: thesis: for A being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine A,i,(a * (Line A,j))) = 0. K
let A be Matrix of n,K; :: thesis: for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine A,i,(a * (Line A,j))) = 0. K
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n & i <> j implies Det (RLine A,i,(a * (Line A,j))) = 0. K )
assume that
A1: i in Seg n and
A2: j in Seg n and
A3: i <> j ; :: thesis: Det (RLine A,i,(a * (Line A,j))) = 0. K
width A = n by MATRIX_1:25;
then len (Line A,j) = n by MATRIX_1:def 8;
hence Det (RLine A,i,(a * (Line A,j))) = a * (Det (RLine A,i,(Line A,j))) by A1, Th34
.= a * (0. K) by A1, A2, A3, Th51
.= 0. K by VECTSP_1:36 ;
:: thesis: verum