let n, m 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 )
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 )
defpred S₁[ set , set ] means ex i being Nat st
( i in Seg m & Line M,i = $1 & $2 = i );
A2: for x being set st x in U holds
ex y being set st
( y in Seg m & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in U implies ex y being set st
( y in Seg m & S₁[x,y] ) )
assume A3: x in U ; :: thesis: ex y being set st
( y in Seg m & S₁[x,y] )
consider i being Nat such that
A4: ( i in Seg m & x = Line M,i ) by A1, A3, Th103;
take i ; :: thesis: ( i in Seg m & S₁[x,i] )
thus ( i in Seg m & S₁[x,i] ) by A4; :: thesis: verum

end;

consider f being Function of U,(Seg m) such that
A5: for x being set st x in U holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
A6: ( rng f c= Seg m & not 0 in Seg m ) by RELAT_1:def 19;
then ( rng f is finite Subset of NAT & not 0 in rng f ) by XBOOLE_1:1;
then reconsider P = rng f as finite without_zero Subset of NAT by PSCOMP_1:def 1;
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 )
set S = Segm M,P,(Seg n);
A7: lines (Segm M,P,(Seg n)) c= U

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in lines (Segm M,P,(Seg n)) or x in U )
assume A8: x in lines (Segm M,P,(Seg n)) ; :: thesis: x in U
then consider y being set such that
A9: ( y in dom (Segm M,P,(Seg n)) & (Segm M,P,(Seg n)) . y = x ) by FUNCT_1:def 5;
A10: dom (Segm M,P,(Seg n)) = Seg (len (Segm M,P,(Seg n))) by FINSEQ_1:def 3
.= Seg (card P) by MATRIX_1:def 3 ;
reconsider y = y as Element of NAT by A9;
dom (Sgm P) = Seg (card P) by A6, FINSEQ_3:45;
then ( (Sgm P) . y in rng (Sgm P) & rng (Sgm P) = P & P c= Seg m ) by A6, A9, A10, FINSEQ_1:def 13, FUNCT_1:def 5;
then consider z being set such that
A11: ( z in dom f & f . z = (Sgm P) . y ) by FUNCT_1:def 5;
consider i being Nat such that
A12: ( i in Seg m & Line M,i = z & f . z = i ) by A5, A11;
lines (Segm M,P,(Seg n)) c= lines M by A6, Th118;
then ( M <> {} & len M = m ) by A8, MATRIX_1:def 3;
then m <> 0 ;
then width M = n by Th1;
then z = Line (Segm M,P,(Seg n)),y by A9, A10, A11, A12, Th48
.= x by A9, A10, MATRIX_2:10 ;
hence x in U by A11; :: thesis: verum

end;

U c= lines (Segm M,P,(Seg n))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in lines (Segm M,P,(Seg n)) )
assume A13: x in U ; :: thesis: x in lines (Segm M,P,(Seg n))
then consider i being Nat such that
A14: ( i in Seg m & Line M,i = x & f . x = i ) by A5;
dom f = U by A14, FUNCT_2:def 1;
then i in P by A13, A14, FUNCT_1:def 5;
then i in rng (Sgm P) by A6, FINSEQ_1:def 13;
then consider y being set such that
A15: ( y in dom (Sgm P) & (Sgm P) . y = i ) by FUNCT_1:def 5;
A16: dom (Sgm P) = Seg (card P) by A6, FINSEQ_3:45;
reconsider y = y as Element of NAT by A15;
width M = n by A14, Th1, FINSEQ_1:4;
then Line (Segm M,P,(Seg n)),y = x by A14, A15, A16, Th48;
hence x in lines (Segm M,P,(Seg n)) by A15, A16, Th103; :: thesis: verum

end;

hence U = lines (Segm M,P,(Seg n)) by A7, XBOOLE_0:def 10; :: thesis: Segm M,P,(Seg n) is without_repeated_line
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 A17: ( 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
A18: dom (Segm M,P,(Seg n)) = Seg (len (Segm M,P,(Seg n))) by FINSEQ_1:def 3
.= Seg (card P) by MATRIX_1:def 3 ;
reconsider i1 = x1, i2 = x2 as Element of NAT by A17;
dom (Sgm P) = Seg (card P) by A6, FINSEQ_3:45;
then A19: ( (Sgm P) . i1 in rng (Sgm P) & (Sgm P) . i2 in rng (Sgm P) & rng (Sgm P) = P & P c= Seg m ) by A6, A17, A18, FINSEQ_1:def 13, FUNCT_1:def 5;
then consider y1 being set such that
A20: ( y1 in dom f & f . y1 = (Sgm P) . i1 ) by FUNCT_1:def 5;
consider y2 being set such that
A21: ( y2 in dom f & f . y2 = (Sgm P) . i2 ) by A19, FUNCT_1:def 5;
consider j1 being Nat such that
A22: ( j1 in Seg m & Line M,j1 = y1 & f . y1 = j1 ) by A5, A20;
consider j2 being Nat such that
A23: ( j2 in Seg m & Line M,j2 = y2 & f . y2 = j2 ) by A5, A21;
width M = n by A22, Th1, FINSEQ_1:4;
then ( Line (Segm M,P,(Seg n)),i1 = y1 & Line (Segm M,P,(Seg n)),i2 = y2 & 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 A17, A18, A20, A21, A22, A23, Th48, MATRIX_2:10;
then ( (Sgm P) . i1 = (Sgm P) . i2 & dom (Sgm P) = dom (Segm M,P,(Seg n)) & Sgm P is without_repeated_line ) by A6, A17, A18, A20, A21, FINSEQ_3:45, FINSEQ_3:99;
hence x1 = x2 by A17, FUNCT_1:def 8; :: thesis: verum