let m, n be Nat; :: thesis: for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m & M is without_repeated_line holds
Segm M,P,(Seg n) is without_repeated_line
let K be Field; :: thesis: for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m & M is without_repeated_line holds
Segm M,P,(Seg n) is without_repeated_line
let P be finite without_zero Subset of NAT ; :: thesis: for M being Matrix of m,n,K st P c= Seg m & M is without_repeated_line holds
Segm M,P,(Seg n) is without_repeated_line
let M be Matrix of m,n,K; :: thesis: ( P c= Seg m & M is without_repeated_line implies Segm M,P,(Seg n) is without_repeated_line )
assume that
A1: P c= Seg m and
A2: M is without_repeated_line ; :: thesis: Segm M,P,(Seg n) is without_repeated_line
set S = Segm M,P,(Seg n);
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom (Segm M,P,(Seg n)) or not x2 in dom (Segm M,P,(Seg n)) or not (Segm M,P,(Seg n)) . x1 = (Segm M,P,(Seg n)) . x2 or x1 = x2 )
assume A3: ( x1 in dom (Segm M,P,(Seg n)) & x2 in dom (Segm M,P,(Seg n)) & (Segm M,P,(Seg n)) . x1 = (Segm M,P,(Seg n)) . x2 ) ; :: thesis: x1 = x2
len (Segm M,P,(Seg n)) = card P by MATRIX_1:def 3;
then A4: dom (Segm M,P,(Seg n)) = Seg (card P) by FINSEQ_1:def 3;
reconsider i1 = x1, i2 = x2 as Element of NAT by A3;
Seg m <> {} by A1, A3, A4, FINSEQ_1:4;
then width M = n by Th1, FINSEQ_1:4;
then A5: ( Line (Segm M,P,(Seg n)),i1 = Line M,((Sgm P) . i1) & Line (Segm M,P,(Seg n)),i2 = Line M,((Sgm P) . i2) & Line (Segm M,P,(Seg n)),i1 = (Segm M,P,(Seg n)) . i1 & Line (Segm M,P,(Seg n)),i2 = (Segm M,P,(Seg n)) . i2 ) by A3, A4, Th48, MATRIX_2:10;
A6: ( dom (Sgm P) = dom (Segm M,P,(Seg n)) & rng (Sgm P) = P ) by A1, A4, FINSEQ_1:def 13, FINSEQ_3:45;
then ( (Sgm P) . i1 in P & (Sgm P) . i2 in P ) by A3, FUNCT_1:def 5;
then ( (Sgm P) . i1 in Seg m & (Sgm P) . i2 in Seg m & len M = m ) by A1, MATRIX_1:def 3;
then ( Line M,((Sgm P) . i1) = M . ((Sgm P) . i1) & Line M,((Sgm P) . i2) = M . ((Sgm P) . i2) & (Sgm P) . i1 in dom M & (Sgm P) . i2 in dom M ) by FINSEQ_1:def 3, MATRIX_2:10;
then ( (Sgm P) . i1 = (Sgm P) . i2 & Sgm P is without_repeated_line ) by A1, A2, A3, A5, FINSEQ_3:99, FUNCT_1:def 8;
hence x1 = x2 by A3, A6, FUNCT_1:def 8; :: thesis: verum