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 object ; :: according to FUNCT_1:def 4 :: 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 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_0:def 2;
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_0:52;
A8: Line ((Segm (M,P,(Seg n))),i2) = (Segm (M,P,(Seg n))) . i2 by A4, A6, MATRIX_0:52;
A9: Sgm P is one-to-one by FINSEQ_3:92;
A10: dom (Sgm P) = dom (Segm (M,P,(Seg n))) by A6, FINSEQ_3:40;
Seg m <> {} by A1, A3, A6;
then m <> 0 ;
then A11: width M = n by Th1;
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_0:def 2;
A15: rng (Sgm P) = P by FINSEQ_1:def 14;
then A16: (Sgm P) . i2 in P by A4, A10, FUNCT_1:def 3;
then A17: Line (M,((Sgm P) . i2)) = M . ((Sgm P) . i2) by A1, MATRIX_0:52;
A18: (Sgm P) . i1 in P by A3, A10, A15, FUNCT_1:def 3;
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_0:52;
then (Sgm P) . i1 = (Sgm P) . i2 by A2, A5, A12, A13, A7, A8, A17, A19, A20;
hence x1 = x2 by A3, A4, A10, A9; :: thesis: verum