let n be Nat; 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; 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; 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; ( not nt is one-to-one implies Det (Segm (M,nt,nt1)) = 0. K )
assume
not nt is one-to-one
; 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; verum