let 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 not nt is one-to-one 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 not nt is one-to-one 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 not nt is one-to-one holds
Det (Segm (M,nt,nt1)) = 0. K
let M be Matrix of K; :: thesis: ( not nt is one-to-one implies Det (Segm (M,nt,nt1)) = 0. K )
assume not nt is one-to-one ; :: thesis: Det (Segm (M,nt,nt1)) = 0. K
then consider x, y being object such that
A1: x in dom nt and
A2: y in dom nt and
A3: nt . x = nt . y and
A4: x <> y ;
A5: dom nt = Seg n by FINSEQ_2:124;
then consider i being Nat such that
A6: x = i and
A7: 1 <= i and
A8: i <= n by A1;
consider j being Nat such that
A9: y = j and
A10: 1 <= j and
A11: j <= n by A2, A5;
A12: j in Seg n by A10, A11;
i in Seg n by A7, A8;
hence Det (Segm (M,nt,nt1)) = 0. K by A3, A4, A6, A9, A12, Th26; :: thesis: verum