let m, n be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K
for U being Subset of (n -VectSp_over K) st U c= lines M holds
ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
let K be Field; :: thesis: for M being Matrix of m,n,K
for U being Subset of (n -VectSp_over K) st U c= lines M holds
ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
let M be Matrix of m,n,K; :: thesis: for U being Subset of (n -VectSp_over K) st U c= lines M holds
ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
defpred S1[ object , object ] means ex i being Nat st
( i in Seg m & Line (M,i) = $1 & $2 = i );
let U be Subset of (n -VectSp_over K); :: thesis: ( U c= lines M implies ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line ) )
assume A1: U c= lines M ; :: thesis: ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
A2: for x being object st x in U holds
ex y being object st
( y in Seg m & S1[x,y] )
proof
let x be object ; :: thesis: ( x in U implies ex y being object st
( y in Seg m & S1[x,y] ) )
assume x in U ; :: thesis: ex y being object st
( y in Seg m & S1[x,y] )
then consider i being Nat such that
A3: i in Seg m and
A4: x = Line (M,i) by A1, Th103;
take i ; :: thesis: ( i in Seg m & S1[x,i] )
thus ( i in Seg m & S1[x,i] ) by A3, A4; :: thesis: verum
end;
consider f being Function of U,(Seg m) such that
A5: for x being object st x in U holds
S1[x,f . x] from FUNCT_2:sch 1(A2);
 A6: rng f c= Seg m by RELAT_1:def 19;
then not 0 in rng f ;
then reconsider P = rng f as finite without_zero Subset of NAT by A6, MEASURE6:def 2, XBOOLE_1:1;
set S = Segm (M,P,(Seg n));
A7: rng (Sgm P) = P by FINSEQ_1:def 14;
A8: lines (Segm (M,P,(Seg n))) c= U
proof
A9: rng (Sgm P) = P by FINSEQ_1:def 14;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lines (Segm (M,P,(Seg n))) or x in U )
A10: dom (Segm (M,P,(Seg n))) = Seg (len (Segm (M,P,(Seg n)))) by FINSEQ_1:def 3
.= Seg (card P) by MATRIX_0:def 2 ;
assume A11: x in lines (Segm (M,P,(Seg n))) ; :: thesis: x in U
then consider y being object such that
A12: y in dom (Segm (M,P,(Seg n))) and
A13: (Segm (M,P,(Seg n))) . y = x by FUNCT_1:def 3;
lines (Segm (M,P,(Seg n))) c= lines M by A6, Th118;
then A14: M <> {} by A11;
len M = m by MATRIX_0:def 2;
then A15: width M = n by A14, Th1;
reconsider y = y as Element of NAT by A12;
dom (Sgm P) = Seg (card P) by FINSEQ_3:40;
then (Sgm P) . y in rng (Sgm P) by A12, A10, FUNCT_1:def 3;
then consider z being object such that
A16: z in dom f and
A17: f . z = (Sgm P) . y by A9, FUNCT_1:def 3;
ex i being Nat st
( i in Seg m & Line (M,i) = z & f . z = i ) by A5, A16;
then z = Line ((Segm (M,P,(Seg n))),y) by A12, A10, A17, A15, Th48
.= x by A12, A13, A10, MATRIX_0:52 ;
hence x in U by A16; :: thesis: verum
end;
take P ; :: thesis: ( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
thus P c= Seg m by RELAT_1:def 19; :: thesis: ( lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )
U c= lines (Segm (M,P,(Seg n)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in lines (Segm (M,P,(Seg n))) )
A18: dom (Sgm P) = Seg (card P) by FINSEQ_3:40;
assume A19: x in U ; :: thesis: x in lines (Segm (M,P,(Seg n)))
then consider i being Nat such that
A20: i in Seg m and
A21: Line (M,i) = x and
A22: f . x = i by A5;
dom f = U by A20, FUNCT_2:def 1;
then i in P by A19, A22, FUNCT_1:def 3;
then i in rng (Sgm P) by FINSEQ_1:def 14;
then consider y being object such that
A23: y in dom (Sgm P) and
A24: (Sgm P) . y = i by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A23;
m <> 0 by A20;
then width M = n by Th1;
then Line ((Segm (M,P,(Seg n))),y) = x by A21, A23, A24, A18, Th48;
hence x in lines (Segm (M,P,(Seg n))) by A23, A18, Th103; :: thesis: verum
end;
hence U = lines (Segm (M,P,(Seg n))) by A8, XBOOLE_0:def 10; :: thesis: Segm (M,P,(Seg n)) is without_repeated_line
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
A25: x1 in dom (Segm (M,P,(Seg n))) and
A26: x2 in dom (Segm (M,P,(Seg n))) and
A27: (Segm (M,P,(Seg n))) . x1 = (Segm (M,P,(Seg n))) . x2 ; :: thesis: x1 = x2
A28: dom (Segm (M,P,(Seg n))) = Seg (len (Segm (M,P,(Seg n)))) by FINSEQ_1:def 3
.= Seg (card P) by MATRIX_0:def 2 ;
then A29: dom (Sgm P) = dom (Segm (M,P,(Seg n))) by FINSEQ_3:40;
reconsider i1 = x1, i2 = x2 as Element of NAT by A25, A26;
A30: dom (Sgm P) = Seg (card P) by FINSEQ_3:40;
then (Sgm P) . i1 in rng (Sgm P) by A25, A28, FUNCT_1:def 3;
then consider y1 being object such that
A31: y1 in dom f and
A32: f . y1 = (Sgm P) . i1 by A7, FUNCT_1:def 3;
A33: ex j1 being Nat st
( j1 in Seg m & Line (M,j1) = y1 & f . y1 = j1 ) by A5, A31;
then m <> 0 ;
then A34: width M = n by Th1;
(Sgm P) . i2 in rng (Sgm P) by A26, A28, A30, FUNCT_1:def 3;
then consider y2 being object such that
A35: y2 in dom f and
A36: f . y2 = (Sgm P) . i2 by A7, FUNCT_1:def 3;
ex j2 being Nat st
( j2 in Seg m & Line (M,j2) = y2 & f . y2 = j2 ) by A5, A35;
then A37: Line ((Segm (M,P,(Seg n))),i2) = y2 by A26, A28, A36, A34, Th48;
A38: Sgm P is one-to-one by FINSEQ_3:92;
A39: Line ((Segm (M,P,(Seg n))),i1) = (Segm (M,P,(Seg n))) . i1 by A25, A28, MATRIX_0:52;
Line ((Segm (M,P,(Seg n))),i1) = y1 by A25, A28, A32, A33, A34, Th48;
then (Sgm P) . i1 = (Sgm P) . i2 by A26, A27, A28, A32, A36, A37, A39, MATRIX_0:52;
hence x1 = x2 by A25, A26, A29, A38; :: thesis: verum