let K be Field; :: thesis:
let M be diagonal Matrix of K; :: thesis:
let NonZero1 be set ; :: thesis:
assume A1: NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * i,i <> 0. K ) } ; :: thesis:
let P, Q be finite without_zero Subset of NAT ; :: thesis:
assume that
A2: [:P,Q:] c= Indices M and
A3: card P = card Q and
A4: Det (EqSegm M,P,Q) <> 0. K ; :: thesis:
set S = Segm M,P,Q;
set SQ = Sgm Q;
set SP = Sgm P;
set ES = EqSegm M,P,Q;
A5: Indices (Segm M,P,Q) = [:(Seg (len (Segm M,P,Q))),(Seg (width (Segm M,P,Q))):] by FINSEQ_1:def 3;
A6: EqSegm M,P,Q = Segm M,P,Q by A3, Def3;
thus P c= NonZero1 :: thesis:

assume not P c= NonZero1 ; :: thesis:
then consider x being set such that
A7: x in P and
A8: not x in NonZero1 by TARSKI:def 3;
A9: P c= Seg (len M) by A2, A3, Th67;
then A10: rng (Sgm P) = P by FINSEQ_1:def 13;
then consider y being set such that
A11: y in dom (Sgm P) and
A12: (Sgm P) . y = x by A7, FUNCT_1:def 5;
reconsider x = x, y = y as Element of NAT by A7, A11;
set L = Line (Segm M,P,Q),y;
A13: dom (Sgm P) = Seg (card P) by A9, FINSEQ_3:45;
Q c= Seg (width M) by A2, A3, Th67;
then A14: rng (Sgm Q) = Q by FINSEQ_1:def 13;

A15: now

let i be Nat; :: thesis:
assume that
A16: 1 <= i and
A17: i <= width (Segm M,P,Q) ; :: thesis:
i in NAT by ORDINAL1:def 13;
then A18: i in Seg (width (Segm M,P,Q)) by A16, A17;
then A19: (Line (Segm M,P,Q),y) . i = (Segm M,P,Q) * y,i by MATRIX_1:def 8;
y in Seg (len (Segm M,P,Q)) by A3, A13, A11, MATRIX_1:25;
then A20: [y,i] in Indices (Segm M,P,Q) by A5, A18, ZFMISC_1:106;
then A21: (Segm M,P,Q) * y,i = M * x,((Sgm Q) . i) by A12, Def1;
A22: (0. K) * (0. K) = 0. K by VECTSP_1:39;
A23: ( (Sgm Q) . i <> x or (Sgm Q) . i = x ) ;
[x,((Sgm Q) . i)] in Indices M by A2, A10, A14, A12, A20, Th17;
then (Line (Segm M,P,Q),y) . i = 0. K by A1, A8, A21, A19, A23, MATRIX_1:def 15;
hence (Line (Segm M,P,Q),y) . i = ((0. K) * (Line (Segm M,P,Q),y)) . i by A18, A22, FVSUM_1:63; :: thesis:

end;

A24: len (Line (Segm M,P,Q),y) = width (Segm M,P,Q) by MATRIX_1:def 8;
len (Line (Segm M,P,Q),y) = len ((0. K) * (Line (Segm M,P,Q),y)) by MATRIXR1:16;
then Line (Segm M,P,Q),y = (0. K) * (Line (Segm M,P,Q),y) by A24, A15, FINSEQ_1:18;
then A25: Det (RLine (EqSegm M,P,Q),y,(Line (EqSegm M,P,Q),y)) = (0. K) * (Det (EqSegm M,P,Q)) by A6, A13, A11, MATRIX11:35;
RLine (EqSegm M,P,Q),y,(Line (EqSegm M,P,Q),y) = EqSegm M,P,Q by MATRIX11:30;
hence contradiction by A4, A25, VECTSP_1:39; :: thesis:

end;

A26: dom (Segm M,P,Q) = Seg (len (Segm M,P,Q)) by FINSEQ_1:def 3;
A27: len (Segm M,P,Q) = card P by A3, MATRIX_1:25;
A28: width (Segm M,P,Q) = card P by A3, MATRIX_1:25;
thus Q c= NonZero1 :: thesis:

A29: Q c= Seg (width M) by A2, A3, Th67;
then A30: dom (Sgm Q) = Seg (card Q) by FINSEQ_3:45;
assume not Q c= NonZero1 ; :: thesis:
then consider x being set such that
A31: x in Q and
A32: not x in NonZero1 by TARSKI:def 3;
A33: rng (Sgm Q) = Q by A29, FINSEQ_1:def 13;
then consider y being set such that
A34: y in dom (Sgm Q) and
A35: (Sgm Q) . y = x by A31, FUNCT_1:def 5;
reconsider x = x, y = y as Element of NAT by A31, A34;
set C = Col (EqSegm M,P,Q),y;
P c= Seg (len M) by A2, A3, Th67;
then A36: rng (Sgm P) = P by FINSEQ_1:def 13;

let k be Element of NAT ; :: thesis:
assume A37: k in Seg (card P) ; :: thesis:
A38: (Segm M,P,Q) * k,y = (Col (EqSegm M,P,Q),y) . k by A6, A27, A26, A37, MATRIX_1:def 9;
A39: [k,y] in Indices (Segm M,P,Q) by A3, A5, A27, A28, A30, A34, A37, ZFMISC_1:106;
then A40: (Segm M,P,Q) * k,y = M * ((Sgm P) . k),x by A35, Def1;
A41: ( (Sgm P) . k <> x or (Sgm P) . k = x ) ;
[((Sgm P) . k),x] in Indices M by A2, A36, A33, A35, A39, Th17;
hence (Col (EqSegm M,P,Q),y) . k = 0. K by A1, A32, A40, A38, A41, MATRIX_1:def 15; :: thesis:

end;

hence contradiction by A3, A4, A30, A34, MATRIX_9:53; :: thesis:

end;