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 without_repeated_line 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 without_repeated_line 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 without_repeated_line holds
Det (Segm M,mt1,mt) = 0. K
let M be Matrix of K; :: thesis: ( not mt is without_repeated_line implies Det (Segm M,mt1,mt) = 0. K )
assume not mt is without_repeated_line ; :: thesis: Det (Segm M,mt1,mt) = 0. K
then consider x, y being set such that
A1: x in dom mt and
A2: y in dom mt and
A3: mt . x = mt . y and
A4: x <> y by FUNCT_1:def 8;
A5: dom mt = Seg m by FINSEQ_2:144;
then consider i being Element of NAT such that
A6: x = i and
A7: 1 <= i and
A8: i <= m by A1;
consider j being Element of 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