let K be Field; :: thesis: for M being Matrix of K
for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 holds
the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1)
let M be Matrix of K; :: thesis: for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 holds
the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1)
let P, P1, Q, Q1 be finite without_zero Subset of NAT ; :: thesis: ( P c= P1 & Q c= Q1 implies the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1) )
assume A1: ( P c= P1 & Q c= Q1 ) ; :: thesis: the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1)
set S = Segm M,P,Q;
set S1 = Segm M,P1,Q1;
consider P2, Q2 being finite without_zero Subset of NAT such that
A2: ( [:P2,Q2:] c= Indices (Segm M,P,Q) & card P2 = card Q2 ) and
A3: ( card P2 = the_rank_of (Segm M,P,Q) & Det (EqSegm (Segm M,P,Q),P2,Q2) <> 0. K ) by Def4;
( P2 = {} iff Q2 = {} ) by A2;
then consider P3, Q3 being finite without_zero Subset of NAT such that
A4: ( P3 c= P & Q3 c= Q ) and
( P3 = (Sgm P) .: P2 & Q3 = (Sgm Q) .: Q2 ) and
A5: ( card P3 = card P2 & card Q3 = card Q2 ) and
A6: Segm (Segm M,P,Q),P2,Q2 = Segm M,P3,Q3 by A2, Th57;
reconsider P4 = (Sgm P1) " P3, Q4 = (Sgm Q1) " Q3 as finite without_zero Subset of NAT by Th53;
consider k being Nat such that
A7: P4 c= Seg k by Th43;
consider k being Nat such that
A8: Q4 c= Seg k by Th43;
( P3 c= P1 & Q3 c= Q1 & rng (Sgm P4) = P4 & rng (Sgm Q4) = Q4 ) by A1, A4, A7, A8, FINSEQ_1:def 13, XBOOLE_1:1;
then A9: ( Segm (Segm M,P1,Q1),P4,Q4 = Segm M,P3,Q3 & card P4 = card P2 & card Q4 = card P2 & [:P4,Q4:] c= Indices (Segm M,P1,Q1) ) by A2, A5, Lm2, Th56;
then EqSegm (Segm M,P,Q),P2,Q2 = Segm (Segm M,P1,Q1),P4,Q4 by A2, A6, Def3
.= EqSegm (Segm M,P1,Q1),P4,Q4 by A9, Def3 ;
hence the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1) by A3, A9, Def4; :: thesis: verum