let K be Field; :: thesis: for M being diagonal Matrix of K
for NonZero being set st NonZero = { 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= NonZero & Q c= NonZero )
let M be diagonal Matrix of K; :: thesis: for NonZero being set st NonZero = { 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= NonZero & Q c= NonZero )
let NonZero be set ; :: thesis: ( NonZero = { 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= NonZero & Q c= NonZero ) )
assume A1: NonZero = { 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= NonZero & Q c= NonZero )
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= NonZero & Q c= NonZero ) )
assume that
A2: ( [:P,Q:] c= Indices M & card P = card Q ) and
A3: Det (EqSegm M,P,Q) <> 0. K ; :: thesis: ( P c= NonZero & Q c= NonZero )
set ES = EqSegm M,P,Q;
set S = Segm M,P,Q;
set SP = Sgm P;
set SQ = Sgm Q;
A4: EqSegm M,P,Q = Segm M,P,Q by A2, Def3;
A5: ( Indices (Segm M,P,Q) = [:(Seg (len (Segm M,P,Q))),(Seg (width (Segm M,P,Q))):] & len (Segm M,P,Q) = card P & dom (Segm M,P,Q) = Seg (len (Segm M,P,Q)) & width (Segm M,P,Q) = card P ) by A2, FINSEQ_1:def 3, MATRIX_1:25;
thus P c= NonZero :: thesis: Q c= NonZero

proof

assume not P c= NonZero ; :: thesis: contradiction
then consider x being set such that
A6: ( x in P & not x in NonZero ) by TARSKI:def 3;
( P c= Seg (len M) & Q c= Seg (width M) ) by A2, Th67;
then A7: ( rng (Sgm P) = P & dom (Sgm P) = Seg (card P) & rng (Sgm Q) = Q ) by FINSEQ_1:def 13, FINSEQ_3:45;
then consider y being set such that
A8: ( y in dom (Sgm P) & (Sgm P) . y = x ) by A6, FUNCT_1:def 5;
reconsider x = x, y = y as Element of NAT by A6, A8;
set L = Line (Segm M,P,Q),y;
A9: ( len (Line (Segm M,P,Q),y) = len ((0. K) * (Line (Segm M,P,Q),y)) & len (Line (Segm M,P,Q),y) = width (Segm M,P,Q) ) by MATRIXR1:16, MATRIX_1:def 8;

now

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 A10: ( 1 <= i & i <= width (Segm M,P,Q) ) ; :: thesis: (Line (Segm M,P,Q),y) . i = ((0. K) * (Line (Segm M,P,Q),y)) . i
i in NAT by ORDINAL1:def 13;
then A11: ( i in Seg (width (Segm M,P,Q)) & y in Seg (len (Segm M,P,Q)) ) by A2, A7, A8, A10, MATRIX_1:25;
then [y,i] in Indices (Segm M,P,Q) by A5, ZFMISC_1:106;
then A12: ( (Segm M,P,Q) * y,i = M * x,((Sgm Q) . i) & [x,((Sgm Q) . i)] in Indices M & (Line (Segm M,P,Q),y) . i = (Segm M,P,Q) * y,i ) by A2, A7, A8, A11, Def1, Th17, MATRIX_1:def 8;
( (Sgm Q) . i <> x or (Sgm Q) . i = x ) ;
then ( (Line (Segm M,P,Q),y) . i = 0. K & (0. K) * (0. K) = 0. K ) by A1, A6, A12, MATRIX_1:def 15, VECTSP_1:39;
hence (Line (Segm M,P,Q),y) . i = ((0. K) * (Line (Segm M,P,Q),y)) . i by A11, FVSUM_1:63; :: thesis: verum

end;

then Line (Segm M,P,Q),y = (0. K) * (Line (Segm M,P,Q),y) by A9, FINSEQ_1:18;
then ( Det (RLine (EqSegm M,P,Q),y,(Line (EqSegm M,P,Q),y)) = (0. K) * (Det (EqSegm M,P,Q)) & RLine (EqSegm M,P,Q),y,(Line (EqSegm M,P,Q),y) = EqSegm M,P,Q ) by A4, A7, A8, MATRIX11:30, MATRIX11:35;
hence contradiction by A3, VECTSP_1:39; :: thesis: verum

end;

thus Q c= NonZero :: thesis: verum

proof

assume not Q c= NonZero ; :: thesis: contradiction
then consider x being set such that
A13: ( x in Q & not x in NonZero ) by TARSKI:def 3;
( P c= Seg (len M) & Q c= Seg (width M) ) by A2, Th67;
then A14: ( rng (Sgm P) = P & dom (Sgm Q) = Seg (card Q) & rng (Sgm Q) = Q ) by FINSEQ_1:def 13, FINSEQ_3:45;
then consider y being set such that
A15: ( y in dom (Sgm Q) & (Sgm Q) . y = x ) by A13, FUNCT_1:def 5;
reconsider x = x, y = y as Element of NAT by A13, A15;
set C = Col (EqSegm M,P,Q),y;

now

let k be Element of NAT ; :: thesis: ( k in Seg (card P) implies (Col (EqSegm M,P,Q),y) . k = 0. K )
assume A16: k in Seg (card P) ; :: thesis: (Col (EqSegm M,P,Q),y) . k = 0. K
[k,y] in Indices (Segm M,P,Q) by A2, A5, A14, A15, A16, ZFMISC_1:106;
then A17: ( (Segm M,P,Q) * k,y = M * ((Sgm P) . k),x & [((Sgm P) . k),x] in Indices M & (Segm M,P,Q) * k,y = (Col (EqSegm M,P,Q),y) . k ) by A2, A4, A5, A14, A15, A16, Def1, Th17, MATRIX_1:def 9;
( (Sgm P) . k <> x or (Sgm P) . k = x ) ;
hence (Col (EqSegm M,P,Q),y) . k = 0. K by A1, A13, A17, MATRIX_1:def 15; :: thesis: verum

end;

hence contradiction by A2, A3, A14, A15, MATRIX_9:53; :: thesis: verum

end;