let K be Field; :: thesis: for M being diagonal Matrix of K
for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 )
let M be diagonal Matrix of K; :: thesis: for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 )
let NonZero1 be set ; :: thesis: ( NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } implies for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 ) )
assume A1: NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } ; :: thesis: for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 )
let P, Q be finite without_zero Subset of NAT; :: thesis: ( [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K implies ( P c= NonZero1 & Q c= NonZero1 ) )
assume that
A2: [:P,Q:] c= Indices M and
A3: card P = card Q and
A4: Det (EqSegm (M,P,Q)) <> 0. K ; :: thesis: ( P c= NonZero1 & Q c= NonZero1 )
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: Q c= NonZero1

proof

assume not P c= NonZero1 ; :: thesis: contradiction
then consider x being object such that
A7: x in P and
A8: not x in NonZero1 ;
A10: rng (Sgm P) = P by FINSEQ_1:def 14;
then consider y being object such that
A11: y in dom (Sgm P) and
A12: (Sgm P) . y = x by A7, FUNCT_1:def 3;
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 FINSEQ_3:40;
A14: rng (Sgm Q) = Q by FINSEQ_1:def 14;

A15: now :: thesis: for i being Nat st 1 <= i & i <= width (Segm (M,P,Q)) holds
(Line ((Segm (M,P,Q)),y)) . i = ((0. K) * (Line ((Segm (M,P,Q)),y))) . i

let i be Nat; :: thesis: ( 1 <= i & i <= width (Segm (M,P,Q)) implies (Line ((Segm (M,P,Q)),y)) . i = ((0. K) * (Line ((Segm (M,P,Q)),y))) . i )
assume that
A16: 1 <= i and
A17: i <= width (Segm (M,P,Q)) ; :: thesis: (Line ((Segm (M,P,Q)),y)) . i = ((0. K) * (Line ((Segm (M,P,Q)),y))) . i
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_0:def 7;
y in Seg (len (Segm (M,P,Q))) by A3, A13, A11, MATRIX_0:24;
then A20: [y,i] in Indices (Segm (M,P,Q)) by A5, A18, ZFMISC_1:87;
then A21: (Segm (M,P,Q)) * (y,i) = M * (x,((Sgm Q) . i)) by A12, Def1;
A22: (0. K) * (0. K) = 0. K ;
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 6;
hence (Line ((Segm (M,P,Q)),y)) . i = ((0. K) * (Line ((Segm (M,P,Q)),y))) . i by A18, A22, FVSUM_1:51; :: thesis: verum

end;

A24: len (Line ((Segm (M,P,Q)),y)) = width (Segm (M,P,Q)) by MATRIX_0:def 7;
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;
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; :: thesis: verum

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_0:24;
A28: width (Segm (M,P,Q)) = card P by A3, MATRIX_0:24;
thus Q c= NonZero1 :: thesis: verum

proof

A30: dom (Sgm Q) = Seg (card Q) by FINSEQ_3:40;
assume not Q c= NonZero1 ; :: thesis: contradiction
then consider x being object such that
A31: x in Q and
A32: not x in NonZero1 ;
A33: rng (Sgm Q) = Q by FINSEQ_1:def 14;
then consider y being object such that
A34: y in dom (Sgm Q) and
A35: (Sgm Q) . y = x by A31, FUNCT_1:def 3;
reconsider x = x, y = y as Element of NAT by A31, A34;
set C = Col ((EqSegm (M,P,Q)),y);
A36: rng (Sgm P) = P by FINSEQ_1:def 14;

now :: thesis: for k being Element of NAT st k in Seg (card P) holds
(Col ((EqSegm (M,P,Q)),y)) . k = 0. K

let k be Element of NAT ; :: thesis: ( k in Seg (card P) implies (Col ((EqSegm (M,P,Q)),y)) . k = 0. K )
assume A37: k in Seg (card P) ; :: thesis: (Col ((EqSegm (M,P,Q)),y)) . k = 0. K
A38: (Segm (M,P,Q)) * (k,y) = (Col ((EqSegm (M,P,Q)),y)) . k by A6, A27, A26, A37, MATRIX_0:def 8;
A39: [k,y] in Indices (Segm (M,P,Q)) by A3, A5, A27, A28, A30, A34, A37, ZFMISC_1:87;
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 6; :: thesis: verum

end;

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

end;