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