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 proj1 (Segm M,P,(Seg n)) or not x2 in proj1 (Segm M,P,(Seg n)) or not (Segm M,P,(Seg n)) . x1 = (Segm M,P,(Seg n)) . x2 or x1 = x2 )
assume that
A3: x1 in dom (Segm M,P,(Seg n)) and
A4: x2 in dom (Segm M,P,(Seg n)) and
A5: (Segm M,P,(Seg n)) . x1 = (Segm M,P,(Seg n)) . x2 ; :: thesis: x1 = x2
reconsider i1 = x1, i2 = x2 as Element of NAT by A3, A4;
len (Segm M,P,(Seg n)) = card P by MATRIX_1:def 3;
then A6: dom (Segm M,P,(Seg n)) = Seg (card P) by FINSEQ_1:def 3;
then A7: Line (Segm M,P,(Seg n)),i1 = (Segm M,P,(Seg n)) . i1 by A3, MATRIX_2:10;
A8: Line (Segm M,P,(Seg n)),i2 = (Segm M,P,(Seg n)) . i2 by A4, A6, MATRIX_2:10;
A9: Sgm P is without_repeated_line by A1, FINSEQ_3:99;
A10: dom (Sgm P) = dom (Segm M,P,(Seg n)) by A1, A6, FINSEQ_3:45;
Seg m <> {} by A1, A3, A6, FINSEQ_1:4;
then m <> 0 ;
then A11: width M = n by Th1, FINSEQ_1:4;
then A12: Line (Segm M,P,(Seg n)),i1 = Line M,((Sgm P) . i1) by A3, A6, Th48;
A13: Line (Segm M,P,(Seg n)),i2 = Line M,((Sgm P) . i2) by A4, A6, A11, Th48;
A14: len M = m by MATRIX_1:def 3;
A15: rng (Sgm P) = P by A1, FINSEQ_1:def 13;
then A16: (Sgm P) . i2 in P by A4, A10, FUNCT_1:def 5;
then A17: Line M,((Sgm P) . i2) = M . ((Sgm P) . i2) by A1, MATRIX_2:10;
A18: (Sgm P) . i1 in P by A3, A10, A15, FUNCT_1:def 5;
then (Sgm P) . i1 in Seg m by A1;
then A19: (Sgm P) . i1 in dom M by A14, FINSEQ_1:def 3;
(Sgm P) . i2 in Seg m by A1, A16;
then A20: (Sgm P) . i2 in dom M by A14, FINSEQ_1:def 3;
Line M,((Sgm P) . i1) = M . ((Sgm P) . i1) by A1, A18, MATRIX_2:10;
then (Sgm P) . i1 = (Sgm P) . i2 by A2, A5, A12, A13, A7, A8, A17, A19, A20, FUNCT_1:def 8;
hence x1 = x2 by A3, A4, A10, A9, FUNCT_1:def 8; :: thesis: verum