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 )
defpred S1[ set , set ] 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 set st x in U holds
ex y being set st
( y in Seg m & S1[x,y] )
proof
let x be set ; :: thesis: ( x in U implies ex y being set st
( y in Seg m & S1[x,y] ) )
assume x in U ; :: thesis: ex y being set 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 set 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 6, XBOOLE_1:1;
set S = Segm M,P,(Seg n);
A7: rng (Sgm P) = P by A6, FINSEQ_1:def 13;
A8: lines (Segm M,P,(Seg n)) c= U
proof
A9: rng (Sgm P) = P by A6, FINSEQ_1:def 13;
let x be set ; :: 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_1:def 3 ;
assume A11: x in lines (Segm M,P,(Seg n)) ; :: thesis: x in U
then consider y being set such that
A12: y in dom (Segm M,P,(Seg n)) and
A13: (Segm M,P,(Seg n)) . y = x by FUNCT_1:def 5;
lines (Segm M,P,(Seg n)) c= lines M by A6, Th118;
then A14: M <> {} by A11;
len M = m by MATRIX_1:def 3;
then A15: width M = n by A14, Th1;
reconsider y = y as Element of NAT by A12;
dom (Sgm P) = Seg (card P) by A6, FINSEQ_3:45;
then (Sgm P) . y in rng (Sgm P) by A12, A10, FUNCT_1:def 5;
then consider z being set such that
A16: z in dom f and
A17: f . z = (Sgm P) . y by A9, FUNCT_1:def 5;
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_2:10 ;
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 set ; :: 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 A6, FINSEQ_3:45;
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 5;
then i in rng (Sgm P) by A6, FINSEQ_1:def 13;
then consider y being set such that
A23: y in dom (Sgm P) and
A24: (Sgm P) . y = i by FUNCT_1:def 5;
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 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
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_1:def 3 ;
then A29: dom (Sgm P) = dom (Segm M,P,(Seg n)) by A6, FINSEQ_3:45;
reconsider i1 = x1, i2 = x2 as Element of NAT by A25, A26;
A30: dom (Sgm P) = Seg (card P) by A6, FINSEQ_3:45;
then (Sgm P) . i1 in rng (Sgm P) by A25, A28, FUNCT_1:def 5;
then consider y1 being set such that
A31: y1 in dom f and
A32: f . y1 = (Sgm P) . i1 by A7, FUNCT_1:def 5;
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 5;
then consider y2 being set such that
A35: y2 in dom f and
A36: f . y2 = (Sgm P) . i2 by A7, FUNCT_1:def 5;
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 without_repeated_line by A6, FINSEQ_3:99;
A39: Line (Segm M,P,(Seg n)),i1 = (Segm M,P,(Seg n)) . i1 by A25, A28, MATRIX_2:10;
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_2:10;
hence x1 = x2 by A25, A26, A29, A38, FUNCT_1:def 8; :: thesis: verum