let i, j, n be Nat; :: thesis: for K being Field
for nt, nt1 being Element of n -tuples_on NAT
for M being Matrix of K st i in Seg n & j in Seg n & nt . i = nt . j & i <> j holds
Det (Segm (M,nt,nt1)) = 0. K
let K be Field; :: thesis: for nt, nt1 being Element of n -tuples_on NAT
for M being Matrix of K st i in Seg n & j in Seg n & nt . i = nt . j & i <> j holds
Det (Segm (M,nt,nt1)) = 0. K
let nt, nt1 be Element of n -tuples_on NAT; :: thesis: for M being Matrix of K st i in Seg n & j in Seg n & nt . i = nt . j & i <> j holds
Det (Segm (M,nt,nt1)) = 0. K
let M be Matrix of K; :: thesis: ( i in Seg n & j in Seg n & nt . i = nt . j & i <> j implies Det (Segm (M,nt,nt1)) = 0. K )
assume that
A1: i in Seg n and
A2: j in Seg n and
A3: nt . i = nt . j and
A4: i <> j ; :: thesis: Det (Segm (M,nt,nt1)) = 0. K
A5: ( i < j or j < i ) by A4, XXREAL_0:1;
Line ((Segm (M,nt,nt1)),i) = Line ((Segm (M,nt,nt1)),j) by A1, A2, A3, Th25;
hence Det (Segm (M,nt,nt1)) = 0. K by A1, A2, A5, MATRIX11:50; :: thesis: verum