let m be Nat; :: thesis: for K being Field
for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st not mt is one-to-one holds
Det (Segm (M,mt1,mt)) = 0. K
let K be Field; :: thesis: for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st not mt is one-to-one holds
Det (Segm (M,mt1,mt)) = 0. K
let mt, mt1 be Element of m -tuples_on NAT; :: thesis: for M being Matrix of K st not mt is one-to-one holds
Det (Segm (M,mt1,mt)) = 0. K
let M be Matrix of K; :: thesis: ( not mt is one-to-one implies Det (Segm (M,mt1,mt)) = 0. K )
assume not mt is one-to-one ; :: thesis: Det (Segm (M,mt1,mt)) = 0. K
then consider x, y being object such that
A1: x in dom mt and
A2: y in dom mt and
A3: mt . x = mt . y and
A4: x <> y ;
A5: dom mt = Seg m by FINSEQ_2:124;
then consider i being Nat such that
A6: x = i and
A7: 1 <= i and
A8: i <= m by A1;
consider j being Nat such that
A9: y = j and
A10: 1 <= j and
A11: j <= m by A2, A5;
A12: j in Seg m by A10, A11;
i in Seg m by A7, A8;
hence Det (Segm (M,mt1,mt)) = 0. K by A3, A4, A6, A9, A12, Th30; :: thesis: verum