matrix_0.miz



    begin

    reserve x,y,z for object,

i,j,n,m for Nat,

D for non empty set,

s,t for FinSequence,

a,a1,a2,b1,b2,d for Element of D,

p,p1,p2,q,r for FinSequence of D;

    definition

      let f be FinSequence;

      :: MATRIX_0:def1

      attr f is tabular means

      : Def1: ex n be Nat st for x st x in ( rng f) holds ex s be FinSequence st s = x & ( len s) = n;

    end

    registration

      cluster tabular for FinSequence;

      existence

      proof

        take M = {} , 0 ;

        let x;

        assume x in ( rng M);

        hence thesis;

      end;

    end

    theorem :: MATRIX_0:1

    

     Th1: <* <*d*>*> is tabular

    proof

      take n = 1;

      let x;

      assume

       A1: x in ( rng <* <*d*>*>);

      

       A2: ( len <*d*>) = n by FINSEQ_1: 39;

      ( rng <* <*d*>*>) = { <*d*>} by FINSEQ_1: 38;

      then x = <*d*> by A1, TARSKI:def 1;

      hence thesis by A2;

    end;

    theorem :: MATRIX_0:2

    

     Th2: (m |-> (n |-> x)) is tabular

    proof

      set s = (m |-> (n |-> x));

      reconsider n1 = n as Nat;

      take n1;

      let z;

      assume

       A1: z in ( rng s);

      take (n |-> x);

      ( rng s) c= {(n |-> x)} by FUNCOP_1: 13;

      hence thesis by A1, CARD_1:def 7, TARSKI:def 1;

    end;

    theorem :: MATRIX_0:3

    

     Th3: <*s*> is tabular

    proof

      take ( len s);

      let x;

      assume x in ( rng <*s*>);

      then

       A1: x in {s} by FINSEQ_1: 38;

      then

      reconsider t = x as FinSequence by TARSKI:def 1;

      take t;

      thus thesis by A1, TARSKI:def 1;

    end;

    theorem :: MATRIX_0:4

    

     Th4: for s1,s2 be FinSequence st ( len s1) = n & ( len s2) = n holds <*s1, s2*> is tabular

    proof

      let s1,s2 be FinSequence;

      assume

       A1: ( len s1) = n & ( len s2) = n;

      take n;

      let x;

      assume x in ( rng <*s1, s2*>);

      then

       A2: x in {s1, s2} by FINSEQ_2: 127;

      then

      reconsider r = x as FinSequence by TARSKI:def 2;

      take r;

      thus x = r & ( len r) = n by A1, A2, TARSKI:def 2;

    end;

    theorem :: MATRIX_0:5

    

     Th5: {} is tabular

    proof

      take n = 0 ;

      let x;

      assume x in ( rng {} );

      hence ex t st t = x & ( len t) = n;

    end;

    theorem :: MATRIX_0:6

     <* {} , {} *> is tabular by Th4, CARD_1: 27;

    theorem :: MATRIX_0:7

     <* <*a1*>, <*a2*>*> is tabular

    proof

      ( len <*a1*>) = 1 & ( len <*a2*>) = 1 by FINSEQ_1: 39;

      hence thesis by Th4;

    end;

    theorem :: MATRIX_0:8

     <* <*a1, a2*>, <*b1, b2*>*> is tabular

    proof

      ( len <*a1, a2*>) = 2 & ( len <*b1, b2*>) = 2 by FINSEQ_1: 44;

      hence thesis by Th4;

    end;

    registration

      let D be set;

      cluster tabular for FinSequence of (D * );

      existence

      proof

        take ( <*> (D * )), 0 ;

        thus thesis;

      end;

    end

    definition

      let D be set;

      mode Matrix of D is tabular FinSequence of (D * );

    end

    registration

      let X be set;

      cluster -> Function-yielding for Matrix of X;

      coherence ;

    end

    registration

      let D be non empty set;

      cluster non empty-yielding for Matrix of D;

      existence

      proof

        set d = the Element of D;

        

         A1: ( rng <* <*d*>*>) = { <*d*>} by FINSEQ_1: 38;

         <*d*> in (D * ) by FINSEQ_1:def 11;

        then ( rng <* <*d*>*>) c= (D * ) by A1, ZFMISC_1: 31;

        then

        reconsider p = <* <*d*>*> as FinSequence of (D * ) by FINSEQ_1:def 4;

        reconsider s = <*d*> as FinSequence;

        reconsider p as tabular FinSequence of (D * ) by Th1;

        take p;

        now

          take s;

          thus s in ( rng p) by A1, TARSKI:def 1;

          thus s <> {} ;

        end;

        hence thesis by RELAT_1: 149;

      end;

    end

    theorem :: MATRIX_0:9

    

     Th9: s is Matrix of D iff ex n st for x st x in ( rng s) holds ex p st x = p & ( len p) = n

    proof

      thus s is Matrix of D implies ex n st for x st x in ( rng s) holds ex p st x = p & ( len p) = n

      proof

        assume s is Matrix of D;

        then

        reconsider s as tabular FinSequence of (D * );

        consider n such that

         A1: for x st x in ( rng s) holds ex t st t = x & ( len t) = n by Def1;

        take n;

        for x st x in ( rng s) holds ex p st x = p & ( len p) = n

        proof

          let x;

          assume

           A2: x in ( rng s);

          then

          consider v be FinSequence such that

           A3: v = x and

           A4: ( len v) = n by A1;

          ( rng s) c= (D * ) by FINSEQ_1:def 4;

          then

          reconsider p = v as FinSequence of D by A2, A3, FINSEQ_1:def 11;

          take p;

          thus thesis by A3, A4;

        end;

        hence thesis;

      end;

      given n such that

       A5: for x st x in ( rng s) holds ex p st x = p & ( len p) = n;

      

       A6: s is tabular

      proof

        consider n such that

         A7: for x st x in ( rng s) holds ex p st x = p & ( len p) = n by A5;

        take n;

        for x st x in ( rng s) holds ex t st t = x & ( len t) = n

        proof

          let x;

          assume x in ( rng s);

          then

          consider p such that

           A8: x = p & ( len p) = n by A7;

          reconsider t = p as FinSequence;

          take t;

          thus thesis by A8;

        end;

        hence thesis;

      end;

      ( rng s) c= (D * )

      proof

        let x be object;

        assume x in ( rng s);

        then ex p st x = p & ( len p) = n by A5;

        then

        reconsider q = x as FinSequence of D;

        q in (D * ) by FINSEQ_1:def 11;

        hence thesis;

      end;

      hence thesis by A6, FINSEQ_1:def 4;

    end;

    definition

      let D;

      let m,n be Nat;

      let M be Matrix of D;

      :: MATRIX_0:def2

      attr M is m,n -size means

      : Def2: ( len M) = m & for p st p in ( rng M) holds ( len p) = n;

    end

    registration

      let D;

      let m,n be Nat;

      cluster m, n -size for Matrix of D;

      existence

      proof

        set a = the Element of D;

        reconsider d = (n |-> a) as Element of (D * ) by FINSEQ_1:def 11;

        reconsider M = (m |-> d) as FinSequence of (D * );

        ex n be Nat st for x st x in ( rng M) holds ex p st x = p & ( len p) = n

        proof

          reconsider p = (n |-> a) as FinSequence of D;

          take n;

          let x;

          assume

           A1: x in ( rng M);

          take p;

          ( rng M) c= {(n |-> a)} by FUNCOP_1: 13;

          hence thesis by A1, CARD_1:def 7, TARSKI:def 1;

        end;

        then

        reconsider M as Matrix of D by Th9;

        take M;

        thus ( len M) = m by CARD_1:def 7;

        let p;

        

         A2: ( rng M) c= {(n |-> a)} by FUNCOP_1: 13;

        assume p in ( rng M);

        then p = (n |-> a) by A2, TARSKI:def 1;

        hence thesis by CARD_1:def 7;

      end;

    end

    definition

      let D;

      let m, n;

      mode Matrix of m,n,D is m, n -size Matrix of D;

    end

    definition

      let D, n;

      mode Matrix of n,D is Matrix of n, n, D;

    end

    theorem :: MATRIX_0:10

    

     Th10: (m |-> (n |-> a)) is Matrix of m, n, D

    proof

      reconsider n1 = n, m1 = m as Nat;

      reconsider d = (n1 |-> a) as Element of (D * ) by FINSEQ_1:def 11;

      reconsider M = (m1 |-> d) as FinSequence of (D * );

      reconsider M as Matrix of D by Th2;

      M is m, n -size

      proof

        thus ( len M) = m by CARD_1:def 7;

        let p;

        

         A1: ( rng M) c= {(n |-> a)} by FUNCOP_1: 13;

        assume p in ( rng M);

        then p = (n |-> a) by A1, TARSKI:def 1;

        hence thesis by CARD_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_0:11

    

     Th11: for p be FinSequence of D holds <*p*> is Matrix of 1, ( len p), D

    proof

      let p be FinSequence of D;

      reconsider p9 = p as Element of (D * ) by FINSEQ_1:def 11;

       <*p9*> is tabular by Th3;

      then

      reconsider M = <*p*> as Matrix of D;

      M is 1, ( len p) -size

      proof

        thus ( len M) = 1 by FINSEQ_1: 39;

        let q;

        assume q in ( rng M);

        then q in {p} by FINSEQ_1: 38;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_0:12

    

     Th12: for p1, p2 st ( len p1) = n & ( len p2) = n holds <*p1, p2*> is Matrix of 2, n, D

    proof

      let p1, p2;

      reconsider q1 = p1, q2 = p2 as Element of (D * ) by FINSEQ_1:def 11;

      reconsider M = <*q1, q2*> as FinSequence of (D * );

      assume

       A1: ( len p1) = n & ( len p2) = n;

      then

      reconsider M as Matrix of D by Th4;

      M is 2, n -size

      proof

        thus ( len M) = 2 by FINSEQ_1: 44;

        let r;

        assume r in ( rng M);

        then r in {p1, p2} by FINSEQ_2: 127;

        hence thesis by A1, TARSKI:def 2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX_0:13

    

     Th13: {} is Matrix of 0 , m, D

    proof

      reconsider M = ( <*> (D * )) as FinSequence of (D * );

      reconsider M as Matrix of D by Th5;

      M is 0 , m -size;

      hence thesis;

    end;

    theorem :: MATRIX_0:14

     <* {} *> is Matrix of 1, 0 , D

    proof

      ( len ( <*> D)) = 0 ;

      hence thesis by Th11;

    end;

    theorem :: MATRIX_0:15

     <* <*a*>*> is Matrix of 1, D

    proof

      ( len <*a*>) = 1 by FINSEQ_1: 39;

      hence thesis by Th11;

    end;

    theorem :: MATRIX_0:16

     <* {} , {} *> is Matrix of 2, 0 , D

    proof

      ( len ( <*> D)) = 0 ;

      hence thesis by Th12;

    end;

    theorem :: MATRIX_0:17

     <* <*a1, a2*>*> is Matrix of 1, 2, D

    proof

       <*a1, a2*> is FinSequence of D & ( len <*a1, a2*>) = 2 by FINSEQ_1: 44;

      hence thesis by Th11;

    end;

    theorem :: MATRIX_0:18

     <* <*a1*>, <*a2*>*> is Matrix of 2, 1, D

    proof

      ( len <*a1*>) = 1 & ( len <*a2*>) = 1 by FINSEQ_1: 39;

      hence thesis by Th12;

    end;

    theorem :: MATRIX_0:19

    

     Th19: <* <*a1, a2*>, <*b1, b2*>*> is Matrix of 2, D

    proof

      

       A1: ( len <*a1, a2*>) = 2 & ( len <*b1, b2*>) = 2 by FINSEQ_1: 44;

      thus thesis by A1, Th12;

    end;

    reserve M,M1,M2 for Matrix of D;

    definition

      let M be tabular FinSequence;

      :: MATRIX_0:def3

      func width M -> Nat means

      : Def3: ex s st s in ( rng M) & ( len s) = it if ( len M) > 0

      otherwise it = 0 ;

      existence

      proof

        thus ( len M) > 0 implies ex n be Nat, s st s in ( rng M) & ( len s) = n

        proof

          set x = the Element of ( rng M);

          consider n such that

           A1: for x st x in ( rng M) holds ex s st s = x & ( len s) = n by Def1;

          reconsider n as Nat;

          assume ( len M) > 0 ;

          then

           A2: ( rng M) <> {} by CARD_1: 27, RELAT_1: 41;

          then

          consider s such that

           A3: s = x & ( len s) = n by A1;

          take n;

          take s;

          thus thesis by A2, A3;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let n1,n2 be Nat;

        thus ( len M) > 0 implies ((ex s st s in ( rng M) & ( len s) = n1) & (ex s st s in ( rng M) & ( len s) = n2) implies n1 = n2)

        proof

          assume ( len M) > 0 ;

          given s such that

           A4: s in ( rng M) and

           A5: ( len s) = n1;

          consider n such that

           A6: for x st x in ( rng M) holds ex s st s = x & ( len s) = n by Def1;

          

           A7: ex s1 be FinSequence st s1 = s & ( len s1) = n by A6, A4;

          given p be FinSequence such that

           A8: p in ( rng M) and

           A9: ( len p) = n2;

          ex p1 be FinSequence st p1 = p & ( len p1) = n by A6, A8;

          hence thesis by A5, A9, A7;

        end;

        thus thesis;

      end;

      consistency ;

    end

    theorem :: MATRIX_0:20

    

     Th20: ( len M) > 0 implies for n holds M is Matrix of ( len M), n, D iff n = ( width M)

    proof

      assume

       A1: ( len M) > 0 ;

      let n;

      thus M is Matrix of ( len M), n, D implies n = ( width M)

      proof

        consider s such that

         A2: s in ( rng M) and

         A3: ( len s) = ( width M) by A1, Def3;

        ( rng M) c= (D * ) by FINSEQ_1:def 4;

        then

        reconsider q = s as FinSequence of D by A2, FINSEQ_1:def 11;

        assume M is Matrix of ( len M), n, D;

        then ( len q) = n by A2, Def2;

        hence thesis by A3;

      end;

      assume n = ( width M);

      then for p st p in ( rng M) holds ( len p) = n by A1, Def3;

      hence thesis by Def2;

    end;

    definition

      let M be tabular FinSequence;

      :: MATRIX_0:def4

      func Indices M -> set equals [:( dom M), ( Seg ( width M)):];

      coherence ;

    end

    definition

      let D be set;

      let M be Matrix of D;

      let i, j;

      assume

       A1: [i, j] in ( Indices M);

      :: MATRIX_0:def5

      func M * (i,j) -> Element of D means

      : Def5: ex p be FinSequence of D st p = (M . i) & it = (p . j);

      existence

      proof

        i in ( dom M) by A1, ZFMISC_1: 87;

        then

         A2: (M . i) in ( rng M) by FUNCT_1:def 3;

        ( rng M) c= (D * ) by FINSEQ_1:def 4;

        then

        reconsider p = (M . i) as FinSequence of D by A2, FINSEQ_1:def 11;

        

         A3: j in ( Seg ( width M)) by A1, ZFMISC_1: 87;

        M <> {} & ( len M) >= 0 by A1, ZFMISC_1: 87;

        then ( len M) > 0 ;

        then

        consider s such that

         A4: s in ( rng M) and

         A5: ( len s) = ( width M) by Def3;

        consider n such that

         A6: for x st x in ( rng M) holds ex t st t = x & ( len t) = n by Def1;

        

         A7: ex v be FinSequence st p = v & ( len v) = n by A2, A6;

        ex t st s = t & ( len t) = n by A4, A6;

        then j in ( dom p) by A3, A5, A7, FINSEQ_1:def 3;

        then

         A8: (p . j) in ( rng p) by FUNCT_1:def 3;

        ( rng p) c= D by FINSEQ_1:def 4;

        then

        reconsider a = (p . j) as Element of D by A8;

        take a, p;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: MATRIX_0:21

    

     Th21: ( len M1) = ( len M2) & ( width M1) = ( width M2) & (for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))) implies M1 = M2

    proof

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( width M1) = ( width M2) and

       A3: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j));

      

       A4: ( dom M1) = ( dom M2) by A1, FINSEQ_3: 29;

      for k be Nat st k in ( dom M1) holds (M1 . k) = (M2 . k)

      proof

        let k be Nat;

        assume

         A5: k in ( dom M1);

        then

         A6: (M1 . k) in ( rng M1) by FUNCT_1:def 3;

        ( rng M1) c= (D * ) by FINSEQ_1:def 4;

        then

        reconsider p = (M1 . k) as FinSequence of D by A6, FINSEQ_1:def 11;

        M1 <> {} by A5;

        then

         A7: ( len M1) > 0 ;

        then M1 is Matrix of ( len M1), ( width M1), D by Th20;

        then

         A8: ( len p) = ( width M1) by A6, Def2;

        

         A9: (M2 . k) in ( rng M2) by A4, A5, FUNCT_1:def 3;

        ( rng M2) c= (D * ) by FINSEQ_1:def 4;

        then

        reconsider q = (M2 . k) as FinSequence of D by A9, FINSEQ_1:def 11;

        M2 is Matrix of ( len M1), ( width M1), D by A1, A2, A7, Th20;

        then

         A10: ( len q) = ( width M1) by A9, Def2;

        for l be Nat st 1 <= l & l <= ( len p) holds (p . l) = (q . l)

        proof

          let l be Nat;

          

           A11: ( rng p) c= D by FINSEQ_1:def 4;

          assume 1 <= l & l <= ( len p);

          then

           A12: l in ( Seg ( width M1)) by A8, FINSEQ_1: 1;

          then l in ( dom p) by A8, FINSEQ_1:def 3;

          then (p . l) in ( rng p) by FUNCT_1:def 3;

          then

          reconsider a = (p . l) as Element of D by A11;

          

           A13: ( rng q) c= D by FINSEQ_1:def 4;

          l in ( dom q) by A10, A12, FINSEQ_1:def 3;

          then (q . l) in ( rng q) by FUNCT_1:def 3;

          then

          reconsider b = (q . l) as Element of D by A13;

           [k, l] in ( Indices M2) by A2, A4, A5, A12, ZFMISC_1: 87;

          then

           A14: (M2 * (k,l)) = b by Def5;

           [k, l] in ( Indices M1) by A5, A12, ZFMISC_1: 87;

          then

           A15: (M1 * (k,l)) = a by Def5;

           [k, l] in [:( dom M1), ( Seg ( width M1)):] by A5, A12, ZFMISC_1: 87;

          hence thesis by A3, A15, A14;

        end;

        hence thesis by A8, A10, FINSEQ_1: 14;

      end;

      hence thesis by A4, FINSEQ_1: 13;

    end;

    scheme :: MATRIX_0:sch1

    MatrixLambda { D() -> non empty set , n,m() -> Nat , f( set, set) -> Element of D() } :

ex M be Matrix of n(), m(), D() st for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = f(i,j);

      defpred P[ set, object] means ex p be FinSequence st $2 = p & ( len p) = m() & for i st i in ( Seg m()) holds (p . i) = f($1,i);

      

       A1: for k be Nat st k in ( Seg n()) holds ex y be object st P[k, y]

      proof

        let k be Nat;

        assume k in ( Seg n());

        deffunc F( Nat) = f(k,$1);

        consider p be FinSequence such that

         A2: ( len p) = m() & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_1:sch 2;

        take p, p;

        ( dom p) = ( Seg m()) by A2, FINSEQ_1:def 3;

        hence thesis by A2;

      end;

      consider M be FinSequence such that

       A3: ( dom M) = ( Seg n()) and

       A4: for k be Nat st k in ( Seg n()) holds P[k, (M . k)] from FINSEQ_1:sch 1( A1);

      n() in NAT by ORDINAL1:def 12;

      then

       A5: ( len M) = n() by A3, FINSEQ_1:def 3;

      ( rng M) c= (D() * )

      proof

        let x be object;

        assume x in ( rng M);

        then

        consider i be Nat such that

         A6: i in ( dom M) and

         A7: (M . i) = x by FINSEQ_2: 10;

        consider p be FinSequence such that

         A8: (M . i) = p and

         A9: ( len p) = m() & for j st j in ( Seg m()) holds (p . j) = f(i,j) by A3, A4, A6;

        ( rng p) c= D()

        proof

          let z be object;

          assume z in ( rng p);

          then

          consider k be Nat such that

           A10: k in ( dom p) and

           A11: (p . k) = z by FINSEQ_2: 10;

          k in ( Seg ( len p)) by A10, FINSEQ_1:def 3;

          then z = f(i,k) by A9, A11;

          hence thesis;

        end;

        then p is FinSequence of D() by FINSEQ_1:def 4;

        hence thesis by A7, A8, FINSEQ_1:def 11;

      end;

      then

      reconsider M as FinSequence of (D() * ) by FINSEQ_1:def 4;

      ex n st for x st x in ( rng M) holds ex p be FinSequence of D() st x = p & ( len p) = n

      proof

        take m();

        let x;

        assume x in ( rng M);

        then

        consider i be Nat such that

         A12: i in ( dom M) & (M . i) = x by FINSEQ_2: 10;

        consider p be FinSequence such that

         A13: x = p and

         A14: ( len p) = m() and

         A15: for j st j in ( Seg m()) holds (p . j) = f(i,j) by A3, A4, A12;

        ( rng p) c= D()

        proof

          let z be object;

          assume z in ( rng p);

          then

          consider k be Nat such that

           A16: k in ( dom p) and

           A17: (p . k) = z by FINSEQ_2: 10;

          k in ( Seg ( len p)) by A16, FINSEQ_1:def 3;

          then z = f(i,k) by A14, A15, A17;

          hence thesis;

        end;

        then

        reconsider p as FinSequence of D() by FINSEQ_1:def 4;

        take p;

        thus thesis by A13, A14;

      end;

      then

      reconsider M as Matrix of D() by Th9;

      for p be FinSequence of D() st p in ( rng M) holds ( len p) = m()

      proof

        let p be FinSequence of D();

        assume p in ( rng M);

        then

        consider i be Nat such that

         A18: i in ( dom M) & (M . i) = p by FINSEQ_2: 10;

         P[i, p] by A3, A4, A18;

        hence thesis;

      end;

      then

      reconsider M as Matrix of n(), m(), D() by A5, Def2;

      take M;

      let i, j;

      assume

       A19: [i, j] in ( Indices M);

      then n() <> 0 by A3, ZFMISC_1: 87;

      then

       A20: n() > 0 ;

      i in ( Seg n()) by A3, A19, ZFMISC_1: 87;

      then

       A21: ex q be FinSequence st (M . i) = q & ( len q) = m() & for j st j in ( Seg m()) holds (q . j) = f(i,j) by A4;

      j in ( Seg ( width M)) by A19, ZFMISC_1: 87;

      then

       A22: j in ( Seg m()) by A5, A20, Th20;

      ex p be FinSequence of D() st p = (M . i) & (M * (i,j)) = (p . j) by A19, Def5;

      hence thesis by A21, A22;

    end;

    scheme :: MATRIX_0:sch2

    MatrixEx { D() -> non empty set , n,m() -> Nat , P[ object, object, object] } :

ex M be Matrix of n(), m(), D() st for i, j st [i, j] in ( Indices M) holds P[i, j, (M * (i,j))]

      provided

       A1: for i, j st [i, j] in [:( Seg n()), ( Seg m()):] holds ex x be Element of D() st P[i, j, x];

      defpred Q[ object, object, object] means P[$1, $2, $3] & $3 in D();

      

       A2: for x, y st x in ( Seg n()) & y in ( Seg m()) holds ex z st z in D() & Q[x, y, z]

      proof

        let x, y;

        assume that

         A3: x in ( Seg n()) and

         A4: y in ( Seg m());

        reconsider y9 = y as Nat by A4;

        reconsider x9 = x as Nat by A3;

         [x9, y9] in [:( Seg n()), ( Seg m()):] by A3, A4, ZFMISC_1: 87;

        then

        consider z9 be Element of D() such that

         A5: P[x9, y9, z9] by A1;

        take z9;

        thus thesis by A5;

      end;

      consider f be Function of [:( Seg n()), ( Seg m()):], D() such that

       A6: for x, y st x in ( Seg n()) & y in ( Seg m()) holds Q[x, y, (f . (x,y))] from BINOP_1:sch 1( A2);

      defpred R[ set, object] means ex p be FinSequence st $2 = p & ( len p) = m() & for i st i in ( Seg m()) holds (p . i) = (f . ($1,i));

      

       A7: for k be Nat st k in ( Seg n()) holds ex y be object st R[k, y]

      proof

        let k be Nat;

        assume k in ( Seg n());

        deffunc F( Nat) = (f . [k, $1]);

        consider p be FinSequence such that

         A8: ( len p) = m() & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_1:sch 2;

        take p, p;

        ( dom p) = ( Seg m()) by A8, FINSEQ_1:def 3;

        hence thesis by A8;

      end;

      consider M be FinSequence such that

       A9: ( dom M) = ( Seg n()) and

       A10: for k be Nat st k in ( Seg n()) holds R[k, (M . k)] from FINSEQ_1:sch 1( A7);

      n() in NAT by ORDINAL1:def 12;

      then

       A11: ( len M) = n() by A9, FINSEQ_1:def 3;

      ( rng M) c= (D() * )

      proof

        let x be object;

        assume x in ( rng M);

        then

        consider i be Nat such that

         A12: i in ( Seg n()) and

         A13: (M . i) = x by A9, FINSEQ_2: 10;

        consider p be FinSequence such that

         A14: (M . i) = p and

         A15: ( len p) = m() and

         A16: for j st j in ( Seg m()) holds (p . j) = (f . (i,j)) by A10, A12;

        ( rng p) c= D()

        proof

          let z be object;

          assume z in ( rng p);

          then

          consider k be Nat such that

           A17: k in ( dom p) and

           A18: (p . k) = z by FINSEQ_2: 10;

          

           A19: k in ( Seg ( len p)) by A17, FINSEQ_1:def 3;

          then

           A20: [i, k] in [:( Seg n()), ( Seg m()):] by A12, A15, ZFMISC_1: 87;

          z = (f . (i,k)) by A15, A16, A18, A19;

          hence thesis by A20, FUNCT_2: 5;

        end;

        then p is FinSequence of D() by FINSEQ_1:def 4;

        hence thesis by A13, A14, FINSEQ_1:def 11;

      end;

      then

      reconsider M as FinSequence of (D() * ) by FINSEQ_1:def 4;

      ex n st for x st x in ( rng M) holds ex p be FinSequence of D() st x = p & ( len p) = n

      proof

        take m();

        let x;

        assume x in ( rng M);

        then

        consider i be Nat such that

         A21: i in ( dom M) and

         A22: (M . i) = x by FINSEQ_2: 10;

        consider p be FinSequence such that

         A23: x = p and

         A24: ( len p) = m() and

         A25: for j st j in ( Seg m()) holds (p . j) = (f . (i,j)) by A9, A10, A21, A22;

        ( rng p) c= D()

        proof

          let z be object;

          assume z in ( rng p);

          then

          consider k be Nat such that

           A26: k in ( dom p) and

           A27: (p . k) = z by FINSEQ_2: 10;

          

           A28: k in ( Seg ( len p)) by A26, FINSEQ_1:def 3;

          then

           A29: [i, k] in [:( Seg n()), ( Seg m()):] by A9, A21, A24, ZFMISC_1: 87;

          z = (f . (i,k)) by A24, A25, A27, A28;

          hence thesis by A29, FUNCT_2: 5;

        end;

        then

        reconsider p as FinSequence of D() by FINSEQ_1:def 4;

        take p;

        thus thesis by A23, A24;

      end;

      then

      reconsider M as Matrix of D() by Th9;

      for p be FinSequence of D() st p in ( rng M) holds ( len p) = m()

      proof

        let p be FinSequence of D();

        assume p in ( rng M);

        then

        consider i be Nat such that

         A30: i in ( dom M) & (M . i) = p by FINSEQ_2: 10;

         R[i, p] by A9, A10, A30;

        hence thesis;

      end;

      then

      reconsider M as Matrix of n(), m(), D() by A11, Def2;

      take M;

      let i, j;

      assume

       A31: [i, j] in ( Indices M);

      then n() <> 0 by A9, ZFMISC_1: 87;

      then

       A32: n() > 0 ;

      j in ( Seg ( width M)) by A31, ZFMISC_1: 87;

      then

       A33: j in ( Seg m()) by A11, A32, Th20;

      

       A34: ex p be FinSequence of D() st p = (M . i) & (M * (i,j)) = (p . j) by A31, Def5;

      

       A35: i in ( Seg n()) by A9, A31, ZFMISC_1: 87;

      then ex q be FinSequence st (M . i) = q & ( len q) = m() & for j st j in ( Seg m()) holds (q . j) = (f . (i,j)) by A10;

      then (f . (i,j)) = (M * (i,j)) by A34, A33;

      hence thesis by A6, A35, A33;

    end;

    theorem :: MATRIX_0:22

    for M be Matrix of 0 , m, D holds ( len M) = 0 & ( width M) = 0 & ( Indices M) = {}

    proof

      let M be Matrix of 0 , m, D;

      ( len M) = 0 by Def2;

      then ( width M) = 0 by Def3;

      then ( Seg ( width M)) = 0 ;

      hence thesis by Def2, ZFMISC_1: 90;

    end;

    theorem :: MATRIX_0:23

    

     Th23: n > 0 implies for M be Matrix of n, m, D holds ( len M) = n & ( width M) = m & ( Indices M) = [:( Seg n), ( Seg m):]

    proof

      assume

       A1: n > 0 ;

      let M be Matrix of n, m, D;

      ( Seg ( len M)) = ( dom M) & ( len M) = n by Def2, FINSEQ_1:def 3;

      hence thesis by A1, Th20;

    end;

    theorem :: MATRIX_0:24

    

     Th24: for M be Matrix of n, D holds ( len M) = n & ( width M) = n & ( Indices M) = [:( Seg n), ( Seg n):]

    proof

      let M be Matrix of n, D;

      

       A1: ( len M) = n by Def2;

       A2:

      now

        per cases ;

          case n = 0 ;

          hence ( width M) = 0 by A1, Def3;

        end;

          case n > 0 ;

          hence ( width M) = n by A1, Th20;

        end;

      end;

      ( Seg ( len M)) = ( dom M) by FINSEQ_1:def 3;

      hence thesis by A2, Def2;

    end;

    theorem :: MATRIX_0:25

    

     Th25: for M be Matrix of n, m, D holds ( len M) = n & ( Indices M) = [:( Seg n), ( Seg ( width M)):]

    proof

      let M be Matrix of n, m, D;

      ( len M) = n by Def2;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: MATRIX_0:26

    for M1,M2 be Matrix of n, m, D holds ( Indices M1) = ( Indices M2)

    proof

      let M1,M2 be Matrix of n, m, D;

      

       A1: ( len M1) = n by Def2;

      

       A2: ( len M2) = n by Def2;

       A3:

      now

        per cases ;

          suppose

           A4: n = 0 ;

          then ( width M1) = 0 by A1, Def3;

          hence ( width M1) = ( width M2) by A2, A4, Def3;

        end;

          suppose

           A5: n > 0 ;

          then ( width M1) = m by A1, Th20;

          hence ( width M1) = ( width M2) by A2, A5, Th20;

        end;

      end;

      ( dom M1) = ( Seg n) by A1, FINSEQ_1:def 3;

      hence thesis by A2, A3, FINSEQ_1:def 3;

    end;

    theorem :: MATRIX_0:27

    for M1,M2 be Matrix of n, m, D st (for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))) holds M1 = M2

    proof

      let M1,M2 be Matrix of n, m, D;

      

       A1: ( len M1) = n by Th25;

      

       A2: ( len M2) = n by Th25;

       A3:

      now

        per cases ;

          suppose

           A4: n = 0 ;

          then ( width M1) = 0 by A1, Def3;

          hence ( width M1) = ( width M2) by A2, A4, Def3;

        end;

          suppose

           A5: n > 0 ;

          then ( width M1) = m by A1, Th20;

          hence ( width M1) = ( width M2) by A2, A5, Th20;

        end;

      end;

      assume for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j));

      hence thesis by A1, A2, A3, Th21;

    end;

    theorem :: MATRIX_0:28

    for M1 be Matrix of n, D holds for i, j st [i, j] in ( Indices M1) holds [j, i] in ( Indices M1)

    proof

      let M1 be Matrix of n, D;

      let i, j;

      assume [i, j] in ( Indices M1);

      then [i, j] in [:( Seg n), ( Seg n):] by Th24;

      then

       A1: j in ( Seg n) & i in ( Seg n) by ZFMISC_1: 87;

      ( Indices M1) = [:( Seg n), ( Seg n):] by Th24;

      hence thesis by A1, ZFMISC_1: 87;

    end;

    definition

      let D;

      let M be Matrix of D;

      :: MATRIX_0:def6

      func M @ -> Matrix of D means

      : Def6: ( len it ) = ( width M) & (for i, j holds [i, j] in ( Indices it ) iff [j, i] in ( Indices M)) & for i, j st [j, i] in ( Indices M) holds (it * (i,j)) = (M * (j,i));

      existence

      proof

        now

          per cases ;

            suppose

             A1: ( width M) > 0 ;

            deffunc F( Nat, Nat) = (M * ($2,$1));

            consider M1 be Matrix of ( width M), ( len M), D such that

             A2: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = F(i,j) from MatrixLambda;

            reconsider M9 = M1 as Matrix of D;

            ( Seg ( len M)) = ( dom M) by FINSEQ_1:def 3;

            then

             A3: ( Indices M1) = [:( Seg ( width M)), ( dom M):] by A1, Th23;

            thus thesis

            proof

              take M9;

              thus ( len M9) = ( width M) by A1, Th23;

              thus for i, j holds [i, j] in ( Indices M9) iff [j, i] in ( Indices M) by A3, ZFMISC_1: 88;

              let i, j;

              assume [j, i] in ( Indices M);

              then [i, j] in ( Indices M9) by A3, ZFMISC_1: 88;

              hence thesis by A2;

            end;

          end;

            suppose

             A4: ( width M) = 0 ;

            reconsider M1 = {} as Matrix of D by Th13;

            thus thesis

            proof

              take M1;

              

               A5: ( Indices M1) = [: {} , ( Seg ( width M1)):];

              ( Seg ( width M)) = {} by A4;

              hence thesis by A5, ZFMISC_1: 90;

            end;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of D;

        assume that

         A6: ( len M1) = ( width M) and

         A7: for i, j holds [i, j] in ( Indices M1) iff [j, i] in ( Indices M) and

         A8: for i, j st [j, i] in ( Indices M) holds (M1 * (i,j)) = (M * (j,i)) and

         A9: ( len M2) = ( width M) and

         A10: for i, j holds [i, j] in ( Indices M2) iff [j, i] in ( Indices M) and

         A11: for i, j st [j, i] in ( Indices M) holds (M2 * (i,j)) = (M * (j,i));

         A12:

        now

          let i, j;

          assume [i, j] in ( Indices M1);

          then

           A13: [j, i] in ( Indices M) by A7;

          then (M1 * (i,j)) = (M * (j,i)) by A8;

          hence (M1 * (i,j)) = (M2 * (i,j)) by A11, A13;

        end;

        now

          let x,y be object;

          thus [x, y] in [:( dom M1), ( Seg ( width M1)):] implies [x, y] in [:( dom M2), ( Seg ( width M2)):]

          proof

            assume

             A14: [x, y] in [:( dom M1), ( Seg ( width M1)):];

            then x in ( dom M1) by ZFMISC_1: 87;

            then

            reconsider i = x as Nat;

            y in ( Seg ( width M1)) by A14, ZFMISC_1: 87;

            then

            reconsider j = y as Nat;

             [j, i] in ( Indices M) by A7, A14;

            hence thesis by A10;

          end;

          thus [x, y] in [:( dom M2), ( Seg ( width M2)):] implies [x, y] in [:( dom M1), ( Seg ( width M1)):]

          proof

            assume

             A15: [x, y] in [:( dom M2), ( Seg ( width M2)):];

            then x in ( dom M2) by ZFMISC_1: 87;

            then

            reconsider i = x as Nat;

            y in ( Seg ( width M2)) by A15, ZFMISC_1: 87;

            then

            reconsider j = y as Nat;

             [j, i] in ( Indices M) by A10, A15;

            hence thesis by A7;

          end;

        end;

        then

         A16: [:( dom M1), ( Seg ( width M1)):] = [:( dom M2), ( Seg ( width M2)):] by ZFMISC_1: 89;

         A17:

        now

          assume

           A18: ( len M1) <> 0 ;

          then ( Seg ( len M2)) <> {} by A6, A9;

          then

           A19: ( dom M2) <> {} by FINSEQ_1:def 3;

          now

            per cases ;

              suppose

               A20: ( Seg ( width M1)) <> {} ;

              ( Seg ( len M1)) <> {} by A18;

              then ( dom M1) <> {} by FINSEQ_1:def 3;

              then ( Seg ( width M1)) = ( Seg ( width M2)) by A16, A20, ZFMISC_1: 110;

              hence ( width M1) = ( width M2) by FINSEQ_1: 6;

            end;

              suppose

               A21: ( Seg ( width M1)) = {} ;

              then [:( dom M2), ( Seg ( width M2)):] = {} by A16, ZFMISC_1: 90;

              then ( Seg ( width M2)) = {} by A19, ZFMISC_1: 90;

              hence ( width M1) = ( width M2) by A21, FINSEQ_1: 6;

            end;

          end;

          hence ( len M1) = ( len M2) & ( width M1) = ( width M2) by A6, A9;

        end;

        ( len M1) = 0 implies ( len M2) = 0 & ( width M1) = 0 & ( width M2) = 0 by A6, A9, Def3;

        hence thesis by A17, A12, Th21;

      end;

    end

    theorem :: MATRIX_0:29

    

     Th29: for M be Matrix of D st ( width M) > 0 holds ( len (M @ )) = ( width M) & ( width (M @ )) = ( len M)

    proof

      let M be Matrix of D;

      assume

       A1: ( width M) > 0 ;

      thus ( len (M @ )) = ( width M) by Def6;

      per cases ;

        suppose ( len M) = 0 ;

        hence thesis by A1, Def3;

      end;

        suppose

         A2: ( len M) > 0 ;

        

         A3: ( width (M @ )) in NAT by ORDINAL1:def 12;

        for i,j be object holds [i, j] in [:( dom (M @ )), ( Seg ( width (M @ ))):] iff [i, j] in [:( Seg ( width M)), ( dom M):]

        proof

          let i,j be object;

          thus [i, j] in [:( dom (M @ )), ( Seg ( width (M @ ))):] implies [i, j] in [:( Seg ( width M)), ( dom M):]

          proof

            assume

             A4: [i, j] in [:( dom (M @ )), ( Seg ( width (M @ ))):];

            then i in ( dom (M @ )) & j in ( Seg ( width (M @ ))) by ZFMISC_1: 87;

            then

            reconsider i, j as Nat;

             [i, j] in ( Indices (M @ )) by A4;

            then [j, i] in ( Indices M) by Def6;

            hence thesis by ZFMISC_1: 88;

          end;

          assume

           A5: [i, j] in [:( Seg ( width M)), ( dom M):];

          then i in ( Seg ( width M)) & j in ( dom M) by ZFMISC_1: 87;

          then

          reconsider i, j as Nat;

           [j, i] in ( Indices M) by A5, ZFMISC_1: 88;

          then [i, j] in ( Indices (M @ )) by Def6;

          hence thesis;

        end;

        then ( dom M) = ( Seg ( len M)) & [:( Seg ( width M)), ( dom M):] = [:( dom (M @ )), ( Seg ( width (M @ ))):] by FINSEQ_1:def 3, ZFMISC_1: 89;

        then ( dom M) = ( Seg ( width (M @ ))) by A1, A2, ZFMISC_1: 110;

        hence thesis by FINSEQ_1:def 3, A3;

      end;

    end;

    registration

      let n, D;

      let M be Matrix of n, D;

      cluster (M @ ) -> n, n -size;

      coherence

      proof

        set K = D, A = M;

        

         A1: ( len A) = n by Def2;

        

         A2: for p be FinSequence of K st p in ( rng (A @ )) holds ( len p) = n

        proof

          let p be FinSequence of K;

          consider n2 be Nat such that

           A3: for x st x in ( rng (A @ )) holds ex s be FinSequence st s = x & ( len s) = n2 by Def1;

          

           A4: for p2 be FinSequence of K st p2 in ( rng (A @ )) holds ( len p2) = n2

          proof

            let p2 be FinSequence of K;

            assume p2 in ( rng (A @ ));

            then ex s be FinSequence st s = p2 & ( len s) = n2 by A3;

            hence thesis;

          end;

          assume

           A5: p in ( rng (A @ ));

          then

           A6: ex s be FinSequence st s = p & ( len s) = n2 by A3;

          per cases ;

            suppose

             A7: n > 0 ;

            then

             A8: ( width A) = n by A1, Th20;

            then

             A9: ( width (A @ )) = ( len A) by A7, Th29;

            

             A10: ( len (A @ )) = ( width A) by A7, A8, Th29;

            then (A @ ) is Matrix of n, n2, K by A4, A8, Def2;

            hence thesis by A1, A6, A7, A8, A10, A9, Th20;

          end;

            suppose

             A11: n <= 0 ;

            

             A12: ( len (A @ )) = ( width A) & ex x0 be object st x0 in ( dom (A @ )) & p = ((A @ ) . x0) by A5, Def6, FUNCT_1:def 3;

            ( width A) = 0 by A1, A11, Def3;

            then ( Seg ( width A)) = {} ;

            hence thesis by A12, FINSEQ_1:def 3;

          end;

        end;

        

         A13: ( len (A @ )) = ( width A) by Def6;

        now

          per cases ;

            suppose n > 0 ;

            hence ( len (A @ )) = n by A13, A1, Th20;

          end;

            suppose n = 0 ;

            hence ( len (A @ )) = n by A13, A1, Def3;

          end;

        end;

        hence thesis by A2;

      end;

    end

    definition

      let D, M, i;

      :: MATRIX_0:def7

      func Line (M,i) -> FinSequence of D means

      : Def7: ( len it ) = ( width M) & for j st j in ( Seg ( width M)) holds (it . j) = (M * (i,j));

      existence

      proof

        deffunc F( Nat) = (M * (i,$1));

        consider f be FinSequence of D such that

         A1: ( len f) = ( width M) and

         A2: for j be Nat st j in ( dom f) holds (f . j) = F(j) from FINSEQ_2:sch 1;

        take f;

        thus ( len f) = ( width M) by A1;

        let j;

        ( dom f) = ( Seg ( width M)) by A1, FINSEQ_1:def 3;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of D;

        assume that

         A3: ( len p1) = ( width M) and

         A4: for j st j in ( Seg ( width M)) holds (p1 . j) = (M * (i,j)) and

         A5: ( len p2) = ( width M) and

         A6: for j st j in ( Seg ( width M)) holds (p2 . j) = (M * (i,j));

        

         A7: ( dom p1) = ( Seg ( width M)) by A3, FINSEQ_1:def 3;

        for j be Nat st j in ( dom p1) holds (p1 . j) = (p2 . j)

        proof

          let j be Nat;

          assume

           A8: j in ( dom p1);

          then (p1 . j) = (M * (i,j)) by A4, A7;

          hence thesis by A6, A7, A8;

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

      :: MATRIX_0:def8

      func Col (M,i) -> FinSequence of D means

      : Def8: ( len it ) = ( len M) & for j st j in ( dom M) holds (it . j) = (M * (j,i));

      existence

      proof

        deffunc F( Nat) = (M * ($1,i));

        consider z be FinSequence of D such that

         A9: ( len z) = ( len M) and

         A10: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

        take z;

        thus ( len z) = ( len M) by A9;

        let j;

        

         A11: ( Seg ( len M)) = ( dom M) by FINSEQ_1:def 3;

        ( dom z) = ( Seg ( len M)) by A9, FINSEQ_1:def 3;

        hence thesis by A10, A11;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of D;

        assume that

         A12: ( len p1) = ( len M) and

         A13: for j st j in ( dom M) holds (p1 . j) = (M * (j,i)) and

         A14: ( len p2) = ( len M) and

         A15: for j st j in ( dom M) holds (p2 . j) = (M * (j,i));

        

         A16: ( dom p1) = ( Seg ( len M)) by A12, FINSEQ_1:def 3;

        for j be Nat st j in ( dom p1) holds (p1 . j) = (p2 . j)

        proof

          let j be Nat;

          assume j in ( dom p1);

          then

           A17: j in ( dom M) by A16, FINSEQ_1:def 3;

          then (p1 . j) = (M * (j,i)) by A13;

          hence thesis by A15, A17;

        end;

        hence thesis by A12, A14, FINSEQ_2: 9;

      end;

    end

    definition

      let D;

      let M be Matrix of D;

      let i;

      :: original: Line

      redefine

      func Line (M,i) -> Element of (( width M) -tuples_on D) ;

      coherence

      proof

        ( len ( Line (M,i))) = ( width M) & ( Line (M,i)) is Element of (D * ) by Def7, FINSEQ_1:def 11;

        then ( Line (M,i)) in { p where p be Element of (D * ) : ( len p) = ( width M) };

        hence thesis;

      end;

      :: original: Col

      redefine

      func Col (M,i) -> Element of (( len M) -tuples_on D) ;

      coherence

      proof

        ( len ( Col (M,i))) = ( len M) & ( Col (M,i)) is Element of (D * ) by Def8, FINSEQ_1:def 11;

        then ( Col (M,i)) in { p where p be Element of (D * ) : ( len p) = ( len M) };

        hence thesis;

      end;

    end

    theorem :: MATRIX_0:30

    

     Th30: for D be set holds for i, j holds for M be Matrix of D st 1 <= i & i <= ( len M) & 1 <= j & j <= ( width M) holds [i, j] in ( Indices M)

    proof

      let D be set;

      let i, j;

      let M be Matrix of D;

      assume 1 <= i & i <= ( len M) & 1 <= j & j <= ( width M);

      then i in ( dom M) & j in ( Seg ( width M)) by FINSEQ_1: 1, FINSEQ_3: 25;

      hence thesis by ZFMISC_1: 87;

    end;

    theorem :: MATRIX_0:31

    for M be Matrix of n, m, D st 1 <= i & i <= n & 1 <= j & j <= m holds [i, j] in ( Indices M)

    proof

      let M be Matrix of n, m, D such that

       A1: 1 <= i & i <= n and

       A2: 1 <= j & j <= m;

      

       A3: ( len M) = n by Def2;

      per cases ;

        suppose n = 0 ;

        hence thesis by A1;

      end;

        suppose n > 0 ;

        then m = ( width M) by Th23;

        hence thesis by A1, A2, A3, Th30;

      end;

    end;

    theorem :: MATRIX_0:32

    

     Th32: for M be tabular FinSequence, i, j st [i, j] in ( Indices M) holds 1 <= i & i <= ( len M) & 1 <= j & j <= ( width M)

    proof

      let M be tabular FinSequence, i, j;

      assume [i, j] in ( Indices M);

      then i in ( dom M) & j in ( Seg ( width M)) by ZFMISC_1: 87;

      hence thesis by FINSEQ_1: 1, FINSEQ_3: 25;

    end;

    theorem :: MATRIX_0:33

    for M be Matrix of n, m, D st [i, j] in ( Indices M) holds 1 <= i & i <= n & 1 <= j & j <= m

    proof

      let M be Matrix of n, m, D such that

       A1: [i, j] in ( Indices M);

      

       A2: ( len M) = n by Def2;

      per cases ;

        suppose

         A3: n = 0 ;

        

         A4: i in ( dom M) by A1, ZFMISC_1: 87;

        then

         A5: 1 <= i by FINSEQ_3: 25;

        i <= 0 by A2, A3, A4, FINSEQ_3: 25;

        hence thesis by A5;

      end;

        suppose n > 0 ;

        then m = ( width M) by Th23;

        hence thesis by A1, A2, Th32;

      end;

    end;

    definition

      let F be Function-yielding Function;

      :: MATRIX_0:def9

      func Values F -> set equals ( Union ( rngs F));

      correctness ;

    end

    theorem :: MATRIX_0:34

    

     Th34: for M be FinSequence of (D * ) holds (M . i) is FinSequence of D

    proof

      let M be FinSequence of (D * );

      per cases ;

        suppose not i in ( dom M);

        then (M . i) = ( <*> D) by FUNCT_1:def 2;

        hence thesis;

      end;

        suppose

         A1: i in ( dom M);

        

         A2: ( rng M) c= (D * ) by FINSEQ_1:def 4;

        (M . i) in ( rng M) by A1, FUNCT_1:def 3;

        hence thesis by A2, FINSEQ_1:def 11;

      end;

    end;

    theorem :: MATRIX_0:35

    

     Th35: for M be FinSequence of (D * ) holds ( Values M) = ( union { ( rng f) where f be Element of (D * ) : f in ( rng M) })

    proof

      let M be FinSequence of (D * );

      set R = { ( rng f) where f be Element of (D * ) : f in ( rng M) };

      

       A1: ( Union ( rngs M)) = ( union ( rng ( rngs M))) by CARD_3:def 4;

      now

        let y be object;

        hereby

          assume y in ( Values M);

          then

          consider Y be set such that

           A2: y in Y and

           A3: Y in ( rng ( rngs M)) by A1, TARSKI:def 4;

          consider i be object such that

           A4: i in ( dom ( rngs M)) and

           A5: (( rngs M) . i) = Y by A3, FUNCT_1:def 3;

          

           A6: i in ( dom M) by A4, FUNCT_6: 60;

          then

          reconsider i as Nat;

          reconsider f = (M . i) as FinSequence of D by Th34;

          

           A7: Y = ( rng f) by A5, A6, FUNCT_6: 22;

          

           A8: f in (D * ) by FINSEQ_1:def 11;

          f in ( rng M) by A6, FUNCT_1:def 3;

          then ( rng f) in R by A8;

          hence y in ( union R) by A2, A7, TARSKI:def 4;

        end;

        assume y in ( union R);

        then

        consider Y be set such that

         A9: y in Y and

         A10: Y in R by TARSKI:def 4;

        consider f be Element of (D * ) such that

         A11: Y = ( rng f) and

         A12: f in ( rng M) by A10;

        consider i be Nat such that

         A13: i in ( dom M) & (M . i) = f by A12, FINSEQ_2: 10;

        i in ( dom ( rngs M)) & (( rngs M) . i) = ( rng f) by A13, FUNCT_6: 22;

        then ( rng f) in ( rng ( rngs M)) by FUNCT_1:def 3;

        hence y in ( Values M) by A1, A9, A11, TARSKI:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let D be non empty set, M be FinSequence of (D * );

      cluster ( Values M) -> finite;

      coherence

      proof

        deffunc F( Function) = ( rng $1);

        set A = { F(f) where f be Element of (D * ) : f in ( rng M) };

         A1:

        now

          let X be set;

          assume X in A;

          then ex f be Element of (D * ) st X = ( rng f) & f in ( rng M);

          hence X is finite;

        end;

        

         A2: ( rng M) is finite;

        { F(f) where f be Element of (D * ) : f in ( rng M) } is finite from FRAENKEL:sch 21( A2);

        then ( union A) is finite by A1, FINSET_1: 7;

        hence thesis by Th35;

      end;

    end

    reserve f for FinSequence of D;

    theorem :: MATRIX_0:36

    

     Th36: for M be Matrix of D st i in ( dom M) & (M . i) = f holds ( len f) = ( width M)

    proof

      let M be Matrix of D such that

       A1: i in ( dom M) and

       A2: (M . i) = f;

      M is non empty by A1;

      then ( len M) > 0 ;

      then

      consider p be FinSequence such that

       A3: p in ( rng M) and

       A4: ( len p) = ( width M) by Def3;

      consider n be Nat such that

       A5: for x st x in ( rng M) holds ex s be FinSequence st s = x & ( len s) = n by Def1;

      (M . i) in ( rng M) by A1, FUNCT_1:def 3;

      then

       A6: ex s be FinSequence st s = (M . i) & ( len s) = n by A5;

      ex s be FinSequence st s = p & ( len s) = n by A3, A5;

      hence thesis by A2, A4, A6;

    end;

    theorem :: MATRIX_0:37

    

     Th37: for M be Matrix of D st i in ( dom M) & (M . i) = f & j in ( dom f) holds [i, j] in ( Indices M)

    proof

      let M be Matrix of D such that

       A1: i in ( dom M) and

       A2: (M . i) = f & j in ( dom f);

      M is non empty by A1;

      then ( len M) > 0 ;

      then

      consider p be FinSequence such that

       A3: p in ( rng M) and

       A4: ( len p) = ( width M) by Def3;

      consider n be Nat such that

       A5: for x st x in ( rng M) holds ex s be FinSequence st s = x & ( len s) = n by Def1;

      (M . i) in ( rng M) by A1, FUNCT_1:def 3;

      then

       A6: ex s be FinSequence st s = (M . i) & ( len s) = n by A5;

      ex s be FinSequence st s = p & ( len s) = n by A3, A5;

      then ( Indices M) = [:( dom M), ( Seg ( width M)):] & j in ( Seg ( width M)) by A2, A4, A6, FINSEQ_1:def 3;

      hence thesis by A1, ZFMISC_1: 87;

    end;

    theorem :: MATRIX_0:38

    

     Th38: for M be Matrix of D st [i, j] in ( Indices M) & (M . i) = f holds ( len f) = ( width M) & j in ( dom f)

    proof

      let M be Matrix of D such that

       A1: [i, j] in ( Indices M);

      

       A2: j in ( Seg ( width M)) by A1, ZFMISC_1: 87;

      M is non empty by A1, ZFMISC_1: 87;

      then ( len M) > 0 ;

      then

      consider p be FinSequence such that

       A3: p in ( rng M) and

       A4: ( len p) = ( width M) by Def3;

      consider n be Nat such that

       A5: for x st x in ( rng M) holds ex s be FinSequence st s = x & ( len s) = n by Def1;

      i in ( dom M) by A1, ZFMISC_1: 87;

      then (M . i) in ( rng M) by FUNCT_1:def 3;

      then

       A6: ex s be FinSequence st s = (M . i) & ( len s) = n by A5;

      ex s be FinSequence st s = p & ( len s) = n by A3, A5;

      hence thesis by A2, A4, A6, FINSEQ_1:def 3;

    end;

    theorem :: MATRIX_0:39

    

     Th39: for M be Matrix of D holds ( Values M) = { (M * (i,j)) where i be Nat, j be Nat : [i, j] in ( Indices M) }

    proof

      let M be Matrix of D;

      set V = { (M * (i,j)) where i be Nat, j be Nat : [i, j] in ( Indices M) }, R = { ( rng f) where f be Element of (D * ) : f in ( rng M) };

      

       A1: ( Values M) = ( union R) by Th35;

      now

        let y be object;

        hereby

          assume y in ( Values M);

          then

          consider Y be set such that

           A2: y in Y and

           A3: Y in R by A1, TARSKI:def 4;

          consider f be Element of (D * ) such that

           A4: Y = ( rng f) and

           A5: f in ( rng M) by A3;

          consider j be Nat such that

           A6: j in ( dom f) and

           A7: (f . j) = y by A2, A4, FINSEQ_2: 10;

          consider i be Nat such that

           A8: i in ( dom M) and

           A9: (M . i) = f by A5, FINSEQ_2: 10;

          reconsider i, j as Nat;

          

           A10: [i, j] in ( Indices M) by A8, A9, A6, Th37;

          then ex p be FinSequence of D st p = (M . i) & (M * (i,j)) = (p . j) by Def5;

          hence y in V by A9, A7, A10;

        end;

        assume y in V;

        then

        consider i,j be Nat such that

         A11: y = (M * (i,j)) and

         A12: [i, j] in ( Indices M);

        consider f be FinSequence of D such that

         A13: f = (M . i) and

         A14: (M * (i,j)) = (f . j) by A12, Def5;

        j in ( dom f) by A12, A13, Th38;

        then

         A15: (f . j) in ( rng f) by FUNCT_1:def 3;

        i in ( dom M) by A12, ZFMISC_1: 87;

        then

         A16: (M . i) in ( rng M) by FUNCT_1:def 3;

        f in (D * ) by FINSEQ_1:def 11;

        then ( rng f) in R by A13, A16;

        hence y in ( Values M) by A1, A11, A14, A15, TARSKI:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: MATRIX_0:40

    for D be non empty set, M be Matrix of D holds ( card ( Values M)) <= (( len M) * ( width M))

    proof

      let D be non empty set, M be Matrix of D;

       A1:

      now

        let x be object;

        assume x in ( dom ( rngs M));

        then

         A2: x in ( dom M) by FUNCT_6: 60;

        then

        reconsider i = x as Element of NAT ;

        reconsider f = (M . i) as FinSequence of D by Th34;

        ( card ( rng f)) c= ( card ( dom f)) by CARD_2: 61;

        then ( card ( rng f)) c= ( card ( Seg ( len f))) by FINSEQ_1:def 3;

        then ( card ( rng f)) c= ( card ( len f)) by FINSEQ_1: 55;

        then ( card ( rng f)) c= ( card ( width M)) by A2, Th36;

        hence ( card (( rngs M) . x)) c= ( card ( width M)) by A2, FUNCT_6: 22;

      end;

      ( card ( dom ( rngs M))) = ( card ( dom M)) by FUNCT_6: 60

      .= ( card ( len M)) by CARD_1: 62;

      then ( card ( Union ( rngs M))) c= (( card ( len M)) *` ( card ( width M))) by A1, CARD_2: 86;

      then ( Segm ( card ( Values M))) c= ( Segm ( card (( len M) * ( width M)))) by CARD_2: 39;

      then ( card ( Values M)) <= ( card (( len M) * ( width M))) by NAT_1: 39;

      hence thesis;

    end;

    reserve i,j,i1,j1 for Nat;

    theorem :: MATRIX_0:41

    for M be Matrix of D st 1 <= i & i <= ( len M) & 1 <= j & j <= ( width M) holds (M * (i,j)) in ( Values M)

    proof

      let M be Matrix of D;

      assume 1 <= i & i <= ( len M) & 1 <= j & j <= ( width M);

      then

       A1: [i, j] in ( Indices M) by Th30;

      ( Values M) = { (M * (i1,j1)) where i1,j1 be Nat : [i1, j1] in ( Indices M) } by Th39;

      hence thesis by A1;

    end;

    theorem :: MATRIX_0:42

    

     Th42: for D be non empty set, M be Matrix of D holds for i, j st j in ( dom M) & i in ( Seg ( width M)) holds (( Col (M,i)) . j) = (( Line (M,j)) . i)

    proof

      let D be non empty set, M be Matrix of D;

      let i, j;

      assume that

       A1: j in ( dom M) and

       A2: i in ( Seg ( width M));

      

      thus (( Col (M,i)) . j) = (M * (j,i)) by A1, Def8

      .= (( Line (M,j)) . i) by A2, Def7;

    end;

    definition

      let D be non empty set;

      let M be Matrix of D;

      :: original: empty-yielding

      redefine

      :: MATRIX_0:def10

      attr M is empty-yielding means 0 = ( len M) or 0 = ( width M);

      compatibility

      proof

        consider n be Nat such that

         A1: for x st x in ( rng M) holds ex s be FinSequence st s = x & ( len s) = n by Def1;

        hereby

          set s = the Element of ( rng M);

          assume

           A2: M is empty-yielding;

          assume

           A3: 0 <> ( len M);

          then

           A4: M <> {} ;

          then ex p be FinSequence st p = s & ( len p) = n by A1;

          then

          reconsider s as FinSequence;

          s = 0 by A2, A4, RELAT_1: 149;

          then ( len s) = 0 ;

          hence 0 = ( width M) by A3, A4, Def3;

        end;

        assume

         A5: 0 = ( len M) or 0 = ( width M);

        now

          let s be set;

          assume

           A6: s in ( rng M);

          then M <> {} ;

          then ( len M) > 0 ;

          then

          consider p be FinSequence such that

           A7: p in ( rng M) and

           A8: ( len p) = 0 by A5, Def3;

          ex q be FinSequence st q = p & ( len q) = n by A1, A7;

          then ex q be FinSequence st q = s & ( len q) = 0 by A1, A6, A8;

          hence s = {} ;

        end;

        hence thesis by RELAT_1: 149;

      end;

    end

    reserve k for Nat,

G for Matrix of D;

    theorem :: MATRIX_0:43

    

     Th43: ( rng f) misses ( rng ( Col (G,i))) & (f /. n) = (G * (m,k)) & n in ( dom f) & m in ( dom G) implies i <> k

    proof

      assume that

       A1: (( rng f) /\ ( rng ( Col (G,i)))) = {} and

       A2: (f /. n) = (G * (m,k)) and

       A3: n in ( dom f) and

       A4: m in ( dom G) and

       A5: i = k;

      (f . n) = (G * (m,k)) by A2, A3, PARTFUN1:def 6;

      then

       A6: (G * (m,i)) in ( rng f) by A3, A5, FUNCT_1:def 3;

      

       A7: ( dom G) = ( Seg ( len G)) & ( dom ( Col (G,i))) = ( Seg ( len ( Col (G,i)))) by FINSEQ_1:def 3;

      ( len ( Col (G,i))) = ( len G) & (( Col (G,i)) . m) = (G * (m,i)) by A4, Def8;

      then (G * (m,i)) in ( rng ( Col (G,i))) by A4, A7, FUNCT_1:def 3;

      hence contradiction by A1, A6, XBOOLE_0:def 4;

    end;

    theorem :: MATRIX_0:44

    for D be non empty set, M be Matrix of D holds M is non empty-yielding iff 0 < ( len M) & 0 < ( width M);

    theorem :: MATRIX_0:45

    for M1 be Matrix of 0 , n, D, M2 be Matrix of 0 , m, D holds M1 = M2

    proof

      let M1 be Matrix of 0 , n, D, M2 be Matrix of 0 , m, D;

      ( len M1) = 0 & ( len M2) = 0 by Def2;

      hence thesis by CARD_2: 64;

    end;

    begin

    reserve x,y,x1,x2,y1,y2 for object,

i,j,k,l,n,m for Nat,

D for non empty set,

s,s2 for FinSequence,

a,b,c,d for Element of D,

q,r for FinSequence of D,

a9,b9 for Element of D;

    definition

      let n, m;

      let a be object;

      :: MATRIX_0:def11

      func (n,m) --> a -> tabular FinSequence equals (n |-> (m |-> a));

      coherence by Th2;

    end

    definition

      let D, n, m;

      let d;

      :: original: -->

      redefine

      func (n,m) --> d -> Matrix of n, m, D ;

      coherence by Th10;

    end

    theorem :: MATRIX_0:46

     [i, j] in ( Indices ((n,m) --> a)) implies (((n,m) --> a) * (i,j)) = a

    proof

      reconsider m1 = m as Nat;

      set M = ((n,m) --> a);

      assume

       A1: [i, j] in ( Indices M);

      then i in ( dom M) by ZFMISC_1: 87;

      then i in ( Seg ( len M)) by FINSEQ_1:def 3;

      then

       A2: i in ( Seg n) by Def2;

      then

       A3: n > 0 ;

      j in ( Seg ( width M)) by A1, ZFMISC_1: 87;

      then j in ( Seg m) by A3, Th23;

      then

       A4: ((m1 |-> a) . j) = a by FUNCOP_1: 7;

      (M . i) = (m1 |-> a) by A2, FUNCOP_1: 7;

      hence thesis by A1, A4, Def5;

    end;

    definition

      let a,b,c,d be object;

      :: MATRIX_0:def12

      func (a,b) ][ (c,d) -> tabular FinSequence equals <* <*a, b*>, <*c, d*>*>;

      correctness

      proof

        ( len <*a, b*>) = 2 & ( len <*c, d*>) = 2 by FINSEQ_1: 44;

        hence thesis by Th4;

      end;

    end

    theorem :: MATRIX_0:47

    

     Th47: ( len ((x1,x2) ][ (y1,y2))) = 2 & ( width ((x1,x2) ][ (y1,y2))) = 2 & ( Indices ((x1,x2) ][ (y1,y2))) = [:( Seg 2), ( Seg 2):]

    proof

      set M = ((x1,x2) ][ (y1,y2));

      thus

       A1: ( len M) = 2 by FINSEQ_1: 44;

      ( rng M) = { <*x1, x2*>, <*y1, y2*>} by FINSEQ_2: 127;

      then

       A2: <*x1, x2*> in ( rng M) by TARSKI:def 2;

      ( len <*x1, x2*>) = 2 by FINSEQ_1: 44;

      hence ( width M) = 2 by A1, A2, Def3;

      hence thesis by A1, FINSEQ_1:def 3;

    end;

    theorem :: MATRIX_0:48

    

     Th48: [1, 1] in ( Indices ((x1,x2) ][ (y1,y2))) & [1, 2] in ( Indices ((x1,x2) ][ (y1,y2))) & [2, 1] in ( Indices ((x1,x2) ][ (y1,y2))) & [2, 2] in ( Indices ((x1,x2) ][ (y1,y2)))

    proof

      

       A1: 2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

      ( Indices ((x1,x2) ][ (y1,y2))) = [:( Seg 2), ( Seg 2):] & 1 in ( Seg 2) by Th47, FINSEQ_1: 2, TARSKI:def 2;

      hence thesis by A1, ZFMISC_1: 87;

    end;

    definition

      let D;

      let a be Element of D;

      :: original: <*

      redefine

      func <*a*> -> Element of (1 -tuples_on D) ;

      coherence by FINSEQ_2: 98;

    end

    definition

      let D;

      let n;

      let p be Element of (n -tuples_on D);

      :: original: <*

      redefine

      func <*p*> -> Matrix of 1, n, D ;

      coherence

      proof

        ( len p) = n by CARD_1:def 7;

        hence thesis by Th11;

      end;

    end

    theorem :: MATRIX_0:49

     [1, 1] in ( Indices <* <*a*>*>) & ( <* <*a*>*> * (1,1)) = a

    proof

      set M = <* <*a*>*>;

      ( Indices M) = [:( Seg 1), ( Seg 1):] & 1 in ( Seg 1) by Th24, FINSEQ_1: 2, TARSKI:def 1;

      hence

       A1: [1, 1] in ( Indices <* <*a*>*>) by ZFMISC_1: 87;

      (M . 1) = <*a*> & ( <*a*> . 1) = a by FINSEQ_1: 40;

      hence thesis by A1, Def5;

    end;

    definition

      let D;

      let a,b,c,d be Element of D;

      :: original: ][

      redefine

      func (a,b) ][ (c,d) -> Matrix of 2, D ;

      coherence by Th19;

    end

    theorem :: MATRIX_0:50

    (((a,b) ][ (c,d)) * (1,1)) = a & (((a,b) ][ (c,d)) * (1,2)) = b & (((a,b) ][ (c,d)) * (2,1)) = c & (((a,b) ][ (c,d)) * (2,2)) = d

    proof

      set M = ((a,b) ][ (c,d));

      

       A1: (M . 1) = <*a, b*> & (M . 2) = <*c, d*> by FINSEQ_1: 44;

      

       A2: ( <*a, b*> . 1) = a & ( <*a, b*> . 2) = b by FINSEQ_1: 44;

      

       A3: [2, 1] in ( Indices M) & [2, 2] in ( Indices M) by Th48;

      

       A4: ( <*c, d*> . 1) = c & ( <*c, d*> . 2) = d by FINSEQ_1: 44;

       [1, 1] in ( Indices M) & [1, 2] in ( Indices M) by Th48;

      hence thesis by A1, A2, A4, A3, Def5;

    end;

    theorem :: MATRIX_0:51

    for M be Matrix of D st ( len M) = n holds M is Matrix of n, ( width M), D

    proof

      let M be Matrix of D;

      assume that

       A1: ( len M) = n and

       A2: not M is Matrix of n, ( width M), D;

      set m = ( width M);

      per cases by A2, Def2;

        suppose ( len M) <> n;

        hence contradiction by A1;

      end;

        suppose

         A3: ex p be FinSequence of D st p in ( rng M) & not ( len p) = m;

        consider k such that

         A4: for x st x in ( rng M) holds ex q st x = q & ( len q) = k by Th9;

        consider p be FinSequence of D such that

         A5: p in ( rng M) and

         A6: ( len p) <> m by A3;

        reconsider x = p as set;

        

         A7: ex q st x = q & ( len q) = k by A5, A4;

        now

          per cases ;

            suppose n = 0 ;

            then M = {} by A1;

            hence ( len p) = m by A5;

          end;

            suppose n > 0 ;

            then

            consider s be FinSequence such that

             A8: s in ( rng M) and

             A9: ( len s) = ( width M) by A1, Def3;

            reconsider y = s as set;

            ex r st y = r & ( len r) = k by A4, A8;

            hence ( len p) = m by A7, A9;

          end;

        end;

        hence contradiction by A6;

      end;

    end;

    begin

    theorem :: MATRIX_0:52

    

     Th52: for M be Matrix of n, m, D holds for k st k in ( Seg n) holds (M . k) = ( Line (M,k))

    proof

      let M be Matrix of n, m, D;

      let k;

      assume

       A1: k in ( Seg n);

      ( len M) = n & ( dom M) = ( Seg ( len M)) by Th25, FINSEQ_1:def 3;

      then

       A2: (M . k) in ( rng M) by A1, FUNCT_1:def 3;

      per cases ;

        suppose n = 0 ;

        hence thesis by A1;

      end;

        suppose

         A3: 0 < n;

        consider l such that

         A4: for x st x in ( rng M) holds ex p be FinSequence of D st x = p & ( len p) = l by Th9;

        consider p be FinSequence of D such that

         A5: (M . k) = p and ( len p) = l by A2, A4;

        

         A6: ( width M) = m by A3, Th23;

        

         A7: for j st j in ( Seg ( width M)) holds (p . j) = (M * (k,j))

        proof

          let j;

          assume j in ( Seg ( width M));

          then [k, j] in [:( Seg n), ( Seg m):] by A1, A6, ZFMISC_1: 87;

          then [k, j] in ( Indices M) by A3, Th23;

          then ex q be FinSequence of D st q = (M . k) & (M * (k,j)) = (q . j) by Def5;

          hence thesis by A5;

        end;

        ( len p) = ( width M) by A2, A6, A5, Def2;

        hence thesis by A5, A7, Def7;

      end;

    end;

    

     Lm1: for M be Matrix of D holds for k st k in ( dom M) holds (M . k) = ( Line (M,k))

    proof

      let M be Matrix of D;

      let k;

      assume

       A1: k in ( dom M);

      then 1 <= k & k <= ( len M) by FINSEQ_3: 25;

      then

      reconsider N = M as Matrix of ( len M), ( width M), D by Th20;

      k in ( Seg ( len N)) by A1, FINSEQ_1:def 3;

      hence thesis by Th52;

    end;

    definition

      let i, D;

      let M be Matrix of D;

      :: MATRIX_0:def13

      func DelCol (M,i) -> Matrix of D means

      : Def13: ( len it ) = ( len M) & for k st k in ( dom M) holds (it . k) = ( Del (( Line (M,k)),i));

      existence

      proof

        per cases ;

          suppose

           A1: not i in ( Seg ( width M));

          take M;

          thus ( len M) = ( len M);

          let k such that

           A2: k in ( dom M);

          ( len ( Line (M,k))) = ( width M) by Def7;

          then

           A3: not i in ( dom ( Line (M,k))) by A1, FINSEQ_1:def 3;

          

          thus (M . k) = ( Line (M,k)) by A2, Lm1

          .= ( Del (( Line (M,k)),i)) by A3, FINSEQ_3: 104;

        end;

          suppose

           A4: i in ( Seg ( width M));

          defpred P[ Nat, Nat, Element of D] means $3 = (( Del (( Line (M,$1)),i)) . $2);

          per cases ;

            suppose

             A5: ( len M) = 0 ;

            then ( Seg ( len M)) = {} ;

            hence thesis by A4, A5, Def3;

          end;

            suppose

             A6: ( len M) > 0 ;

            set n1 = ( width M);

            per cases ;

              suppose n1 = 0 ;

              hence thesis by A4;

            end;

              suppose n1 > 0 ;

              then

              consider m be Nat such that

               A7: n1 = (m + 1) by NAT_1: 6;

              reconsider m as Nat;

              

               A8: for k st k in ( dom M) holds ( len ( Del (( Line (M,k)),i))) = m

              proof

                let k;

                assume k in ( dom M);

                

                 A9: ( len ( Line (M,k))) = n1 by Def7;

                then i in ( dom ( Line (M,k))) by A4, FINSEQ_1:def 3;

                then ex l be Nat st ( len ( Line (M,k))) = (l + 1) & ( len ( Del (( Line (M,k)),i))) = l by FINSEQ_3: 104;

                hence thesis by A7, A9;

              end;

              

               A10: for k, l st [k, l] in [:( Seg ( len M)), ( Seg m):] holds ex x be Element of D st P[k, l, x]

              proof

                let k, l;

                assume

                 A11: [k, l] in [:( Seg ( len M)), ( Seg m):];

                reconsider p = ( Del (( Line (M,k)),i)) as FinSequence of D by FINSEQ_3: 105;

                ( dom M) = ( Seg ( len M)) by FINSEQ_1:def 3;

                then k in ( dom M) by A11, ZFMISC_1: 87;

                then

                 A12: ( len p) = m by A8;

                

                 A13: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

                l in ( Seg m) by A11, ZFMISC_1: 87;

                then

                reconsider x = (p . l) as Element of D by A12, A13, FINSEQ_2: 11;

                take x;

                thus thesis;

              end;

              consider N be Matrix of ( len M), m, D such that

               A14: for k, l st [k, l] in ( Indices N) holds P[k, l, (N * (k,l))] from MatrixEx( A10);

              ( dom M) = ( Seg ( len M)) by FINSEQ_1:def 3;

              then

               A15: ( Indices N) = [:( dom M), ( Seg m):] by A6, Th23;

              

               A16: for k, l st k in ( dom M) & l in ( Seg m) holds (N * (k,l)) = (( Del (( Line (M,k)),i)) . l)

              proof

                let k, l;

                assume k in ( dom M) & l in ( Seg m);

                then [k, l] in ( Indices N) by A15, ZFMISC_1: 87;

                hence thesis by A14;

              end;

              

               A17: ( width N) = m by A6, Th23;

              reconsider N as Matrix of D;

              take N;

              for k st k in ( dom M) holds (N . k) = ( Del (( Line (M,k)),i))

              proof

                let k;

                assume

                 A18: k in ( dom M);

                then k in ( Seg ( len M)) by FINSEQ_1:def 3;

                then

                 A19: (N . k) = ( Line (N,k)) by Th52;

                reconsider s = (N . k) as FinSequence;

                

                 A20: ( len s) = m by A17, A19, Def7;

                then

                 A21: ( dom s) = ( Seg m) by FINSEQ_1:def 3;

                 A22:

                now

                  let j be Nat;

                  assume

                   A23: j in ( dom s);

                  then (( Line (N,k)) . j) = (N * (k,j)) by A17, A21, Def7;

                  hence (s . j) = (( Del (( Line (M,k)),i)) . j) by A16, A18, A19, A21, A23;

                end;

                ( len ( Del (( Line (M,k)),i))) = m by A8, A18;

                hence thesis by A20, A22, FINSEQ_2: 9;

              end;

              hence thesis by A6, Th23;

            end;

          end;

        end;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of D;

        assume that

         A24: ( len M1) = ( len M) and

         A25: for k st k in ( dom M) holds (M1 . k) = ( Del (( Line (M,k)),i)) and

         A26: ( len M2) = ( len M) and

         A27: for k st k in ( dom M) holds (M2 . k) = ( Del (( Line (M,k)),i));

        

         A28: ( dom M1) = ( dom M) by A24, FINSEQ_3: 29;

        now

          let k be Nat;

          assume

           A29: k in ( dom M1);

          

          hence (M1 . k) = ( Del (( Line (M,k)),i)) by A25, A28

          .= (M2 . k) by A27, A28, A29;

        end;

        hence thesis by A24, A26, FINSEQ_2: 9;

      end;

    end

    theorem :: MATRIX_0:53

    

     Th53: for M1,M2 be Matrix of D st (M1 @ ) = (M2 @ ) & ( len M1) = ( len M2) holds M1 = M2

    proof

      let M1,M2 be Matrix of D;

      assume that

       A1: (M1 @ ) = (M2 @ ) and

       A2: ( len M1) = ( len M2);

      ( len (M1 @ )) = ( width M1) by Def6;

      then

       A3: ( width M1) = ( width M2) by A1, Def6;

      

       A4: ( Indices M2) = [:( dom M2), ( Seg ( width M2)):];

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices M1);

        ( dom M1) = ( Seg ( len M2)) by A2, FINSEQ_1:def 3

        .= ( dom M2) by FINSEQ_1:def 3;

        then ((M2 @ ) * (j,i)) = (M2 * (i,j)) by A3, A4, A5, Def6;

        hence thesis by A1, A5, Def6;

      end;

      hence thesis by A2, A3, Th21;

    end;

    theorem :: MATRIX_0:54

    

     Th54: for M be Matrix of D st ( width M) > 0 holds ( len (M @ )) = ( width M) & ( width (M @ )) = ( len M)

    proof

      let M be Matrix of D;

      assume

       A1: ( width M) > 0 ;

      thus ( len (M @ )) = ( width M) by Def6;

      per cases ;

        suppose ( len M) = 0 ;

        hence thesis by A1, Def3;

      end;

        suppose

         A2: ( len M) > 0 ;

        

         A3: ( width (M @ )) in NAT by ORDINAL1:def 12;

        for i,j be object holds [i, j] in [:( dom (M @ )), ( Seg ( width (M @ ))):] iff [i, j] in [:( Seg ( width M)), ( dom M):]

        proof

          let i,j be object;

          thus [i, j] in [:( dom (M @ )), ( Seg ( width (M @ ))):] implies [i, j] in [:( Seg ( width M)), ( dom M):]

          proof

            assume

             A4: [i, j] in [:( dom (M @ )), ( Seg ( width (M @ ))):];

            then i in ( dom (M @ )) & j in ( Seg ( width (M @ ))) by ZFMISC_1: 87;

            then

            reconsider i, j as Nat;

             [i, j] in ( Indices (M @ )) by A4;

            then [j, i] in ( Indices M) by Def6;

            hence thesis by ZFMISC_1: 88;

          end;

          assume

           A5: [i, j] in [:( Seg ( width M)), ( dom M):];

          then i in ( Seg ( width M)) & j in ( dom M) by ZFMISC_1: 87;

          then

          reconsider i, j as Nat;

           [j, i] in ( Indices M) by A5, ZFMISC_1: 88;

          then [i, j] in ( Indices (M @ )) by Def6;

          hence thesis;

        end;

        then ( dom M) = ( Seg ( len M)) & [:( Seg ( width M)), ( dom M):] = [:( dom (M @ )), ( Seg ( width (M @ ))):] by FINSEQ_1:def 3, ZFMISC_1: 89;

        then ( dom M) = ( Seg ( width (M @ ))) by A1, A2, ZFMISC_1: 110;

        hence thesis by FINSEQ_1:def 3, A3;

      end;

    end;

    theorem :: MATRIX_0:55

    for M1,M2 be Matrix of D st ( width M1) > 0 & ( width M2) > 0 & (M1 @ ) = (M2 @ ) holds M1 = M2

    proof

      let M1,M2 be Matrix of D;

      assume ( width M1) > 0 & ( width M2) > 0 ;

      then

       A1: ( width (M1 @ )) = ( len M1) & ( width (M2 @ )) = ( len M2) by Th54;

      assume (M1 @ ) = (M2 @ );

      hence thesis by A1, Th53;

    end;

    theorem :: MATRIX_0:56

    for M1,M2 be Matrix of D st ( width M1) > 0 & ( width M2) > 0 holds M1 = M2 iff (M1 @ ) = (M2 @ ) & ( width M1) = ( width M2)

    proof

      let M1,M2 be Matrix of D;

      assume that

       A1: ( width M1) > 0 and

       A2: ( width M2) > 0 ;

      thus M1 = M2 implies (M1 @ ) = (M2 @ ) & ( width M1) = ( width M2);

      assume that

       A3: (M1 @ ) = (M2 @ ) and

       A4: ( width M1) = ( width M2);

      ( len M1) = ( width (M1 @ )) by A1, Th54;

      then

       A5: ( len M1) = ( len M2) by A2, A3, Th54;

      

       A6: ( Indices M2) = [:( dom M2), ( Seg ( width M2)):];

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices M1);

        ( dom M1) = ( Seg ( len M2)) by A5, FINSEQ_1:def 3

        .= ( dom M2) by FINSEQ_1:def 3;

        then ((M2 @ ) * (j,i)) = (M2 * (i,j)) by A4, A6, A7, Def6;

        hence thesis by A3, A7, Def6;

      end;

      hence thesis by A4, A5, Th21;

    end;

    theorem :: MATRIX_0:57

    

     Th57: for M be Matrix of D st ( len M) > 0 & ( width M) > 0 holds ((M @ ) @ ) = M

    proof

      let M be Matrix of D;

      assume that

       A1: ( len M) > 0 and

       A2: ( width M) > 0 ;

      set N = (M @ );

      

       A3: ( width N) = ( len M) by A2, Th54;

      

       A4: ( len (N @ )) = ( width N) by Def6;

      

       A5: ( len N) = ( width M) by Def6;

      ( dom M) = ( Seg ( len M)) & ( dom (N @ )) = ( Seg ( len (N @ ))) by FINSEQ_1:def 3;

      then

       A6: ( Indices (N @ )) = ( Indices M) by A1, A5, A3, A4, Th54;

      

       A7: for i, j st [i, j] in ( Indices (N @ )) holds ((N @ ) * (i,j)) = (M * (i,j))

      proof

        let i, j;

        assume

         A8: [i, j] in ( Indices (N @ ));

        then [j, i] in ( Indices N) by Def6;

        then ((N @ ) * (i,j)) = (N * (j,i)) by Def6;

        hence thesis by A6, A8, Def6;

      end;

      ( width N) > 0 by A1, A2, Th54;

      then ( width (N @ )) = ( width M) by A5, Th54;

      hence thesis by A3, A4, A7, Th21;

    end;

    theorem :: MATRIX_0:58

    

     Th58: for M be Matrix of D holds for i st i in ( dom M) holds ( Line (M,i)) = ( Col ((M @ ),i))

    proof

      let M be Matrix of D;

      let i;

      

       A1: ( len (M @ )) = ( width M) by Def6;

      ( len ( Col ((M @ ),i))) = ( len (M @ )) by Def8;

      then

       A2: ( len ( Col ((M @ ),i))) = ( width M) by Def6;

      then

       A3: ( dom ( Col ((M @ ),i))) = ( Seg ( width M)) by FINSEQ_1:def 3;

      assume

       A4: i in ( dom M);

       A5:

      now

        let j be Nat;

        

         A6: ( dom (M @ )) = ( Seg ( len (M @ ))) by FINSEQ_1:def 3;

        assume

         A7: j in ( dom ( Col ((M @ ),i)));

        then (( Line (M,i)) . j) = (M * (i,j)) & [i, j] in ( Indices M) by A4, A3, Def7, ZFMISC_1: 87;

        

        hence (( Line (M,i)) . j) = ((M @ ) * (j,i)) by Def6

        .= (( Col ((M @ ),i)) . j) by A1, A3, A7, A6, Def8;

      end;

      ( len ( Line (M,i))) = ( width M) by Def7;

      hence thesis by A2, A5, FINSEQ_2: 9;

    end;

    theorem :: MATRIX_0:59

    for M be Matrix of D holds for j st j in ( Seg ( width M)) holds ( Line ((M @ ),j)) = ( Col (M,j))

    proof

      let M be Matrix of D;

      let j;

      assume

       A1: j in ( Seg ( width M));

      then j in ( Seg ( len (M @ ))) by Def6;

      then

       A2: j in ( dom (M @ )) by FINSEQ_1:def 3;

      per cases ;

        suppose

         A3: ( len M) = 0 ;

        then ( Seg ( len M)) = {} ;

        hence thesis by A1, A3, Def3;

      end;

        suppose

         A4: ( len M) > 0 ;

        per cases ;

          suppose ( width M) = 0 ;

          hence thesis by A1;

        end;

          suppose ( width M) > 0 ;

          then ((M @ ) @ ) = M by A4, Th57;

          hence thesis by A2, Th58;

        end;

      end;

    end;

    theorem :: MATRIX_0:60

    

     Th60: for M be Matrix of D holds for i st i in ( dom M) holds (M . i) = ( Line (M,i))

    proof

      let M be Matrix of D;

      let i;

      assume

       A1: i in ( dom M);

      then

       A2: (M . i) in ( rng M) by FUNCT_1:def 3;

      ( rng M) c= (D * ) by FINSEQ_1:def 4;

      then

      reconsider p = (M . i) as FinSequence of D by A2, FINSEQ_1:def 11;

      M <> {} by A1;

      then M is Matrix of ( len M), ( width M), D by Th20;

      then

       A3: ( len p) = ( width M) by A2, Def2;

      

       A4: ( len ( Line (M,i))) = ( width M) by Def7;

      then

       A5: ( dom ( Line (M,i))) = ( Seg ( width M)) by FINSEQ_1:def 3;

      

       A6: for j st j in ( Seg ( width M)) holds (M * (i,j)) = (p . j)

      proof

        let j;

        assume j in ( Seg ( width M));

        then [i, j] in ( Indices M) by A1, ZFMISC_1: 87;

        then ex q be FinSequence of D st q = (M . i) & (q . j) = (M * (i,j)) by Def5;

        hence thesis;

      end;

      now

        let j be Nat;

        assume

         A7: j in ( dom ( Line (M,i)));

        

        hence (( Line (M,i)) . j) = (M * (i,j)) by A5, Def7

        .= (p . j) by A6, A5, A7;

      end;

      hence thesis by A3, A4, FINSEQ_2: 9;

    end;

    notation

      let D, i;

      let M be Matrix of D;

      synonym DelLine (M,i) for Del (M,i);

    end

    registration

      let D, i;

      let M be Matrix of D;

      cluster ( DelLine (M,i)) -> tabular;

      coherence

      proof

        consider n be Nat such that

         A1: for x st x in ( rng M) holds ex s be FinSequence st s = x & ( len s) = n by Def1;

        take n;

        let x;

        

         A2: ( rng ( DelLine (M,i))) c= ( rng M) by FINSEQ_3: 106;

        assume x in ( rng ( DelLine (M,i)));

        hence thesis by A1, A2;

      end;

    end

    definition

      let D, i;

      let M be Matrix of D;

      :: original: DelLine

      redefine

      func DelLine (M,i) -> Matrix of D ;

      coherence by FINSEQ_3: 105;

    end

    definition

      let i, j, n, D;

      let M be Matrix of n, D;

      :: MATRIX_0:def14

      func Deleting (M,i,j) -> Matrix of D equals ( DelCol (( DelLine (M,i)),j));

      coherence ;

    end

    theorem :: MATRIX_0:61

     not i in ( Seg ( width M)) implies ( DelCol (M,i)) = M

    proof

      assume

       A1: not i in ( Seg ( width M));

      

       A2: ( len ( DelCol (M,i))) = ( len M) by Def13;

      for k st 1 <= k & k <= ( len M) holds (M . k) = (( DelCol (M,i)) . k)

      proof

        let k such that

         A3: 1 <= k & k <= ( len M);

        

         A4: k in ( dom M) by A3, FINSEQ_3: 25;

        ( len ( Line (M,k))) = ( width M) by Def7;

        then

         A5: not i in ( dom ( Line (M,k))) by A1, FINSEQ_1:def 3;

        

        thus (M . k) = ( Line (M,k)) by A4, Lm1

        .= ( Del (( Line (M,k)),i)) by A5, FINSEQ_3: 104

        .= (( DelCol (M,i)) . k) by A4, Def13;

      end;

      hence ( DelCol (M,i)) = M by A2, FINSEQ_1: 14;

    end;

    theorem :: MATRIX_0:62

    

     Th62: k in ( dom G) implies ( Line (( DelCol (G,i)),k)) = ( Del (( Line (G,k)),i))

    proof

      set D = ( DelCol (G,i));

      assume that

       A1: k in ( dom G);

      ( len D) = ( len G) by Def13;

      then

       A2: ( dom D) = ( dom G) by FINSEQ_3: 29;

      (D . k) = ( Del (( Line (G,k)),i)) by A1, Def13;

      hence thesis by A1, A2, Th60;

    end;

    theorem :: MATRIX_0:63

    

     Th63: i in ( Seg ( width G)) & ( width G) = (m + 1) implies ( width ( DelCol (G,i))) = m

    proof

      set D = ( DelCol (G,i));

      assume that

       A1: i in ( Seg ( width G)) and

       A2: ( width G) = (m + 1);

      ( width G) <> 0 by A2;

      then 0 < ( len G) by Def3;

      then ( 0 + 1) <= ( len G) by NAT_1: 13;

      then 1 in ( dom G) by FINSEQ_3: 25;

      then

       A3: ( Line (D,1)) = ( Del (( Line (G,1)),i)) by Th62;

      

       A4: ( dom ( Line (G,1))) = ( Seg ( len ( Line (G,1)))) & ( len ( Line (D,1))) = ( width D) by Def7, FINSEQ_1:def 3;

      ( len ( Line (G,1))) = (m + 1) by A2, Def7;

      hence thesis by A1, A2, A3, A4, FINSEQ_3: 109;

    end;

    theorem :: MATRIX_0:64

    

     Th64: i in ( Seg ( width G)) & ( width G) > 0 implies ( width G) = (( width ( DelCol (G,i))) + 1)

    proof

      assume that

       A1: i in ( Seg ( width G)) and

       A2: ( width G) > 0 ;

      ex m st ( width G) = (m + 1) by A2, NAT_1: 6;

      hence thesis by A1, Th63;

    end;

    theorem :: MATRIX_0:65

    ( width G) > 1 & i in ( Seg ( width G)) implies not ( DelCol (G,i)) is empty-yielding

    proof

      assume that

       A1: ( width G) > 1 and

       A2: i in ( Seg ( width G));

      (( width ( DelCol (G,i))) + 1) > ( 0 + 1) by A1, A2, Th64;

      then

       A3: ( width ( DelCol (G,i))) > 0 ;

      then ( len ( DelCol (G,i))) > 0 by Def3;

      hence not ( DelCol (G,i)) is empty-yielding by A3;

    end;

    theorem :: MATRIX_0:66

    

     Th66: i in ( Seg ( width G)) & ( width G) > 1 & n in ( dom G) & m in ( Seg ( width ( DelCol (G,i)))) implies (( DelCol (G,i)) * (n,m)) = (( Del (( Line (G,n)),i)) . m)

    proof

      assume that

       A1: i in ( Seg ( width G)) & ( width G) > 1 & n in ( dom G) and

       A2: m in ( Seg ( width ( DelCol (G,i))));

      

      thus (( DelCol (G,i)) * (n,m)) = (( Line (( DelCol (G,i)),n)) . m) by A2, Def7

      .= (( Del (( Line (G,n)),i)) . m) by A1, Th62;

    end;

    reserve m for Nat;

    theorem :: MATRIX_0:67

    

     Th67: i in ( Seg ( width G)) & ( width G) = (m + 1) & m > 0 & 1 <= k & k < i implies ( Col (( DelCol (G,i)),k)) = ( Col (G,k)) & k in ( Seg ( width ( DelCol (G,i)))) & k in ( Seg ( width G))

    proof

      set N = ( DelCol (G,i));

      assume that

       A1: i in ( Seg ( width G)) and

       A2: ( width G) = (m + 1) and

       A3: m > 0 and

       A4: 1 <= k and

       A5: k < i;

      

       A6: ( width N) = m by A1, A2, Th63;

      

       A7: 1 < ( width G) by A2, A3, SEQM_3: 43;

      

       A8: ( len N) = ( len G) by Def13;

      i <= (m + 1) by A1, A2, FINSEQ_1: 1;

      then

       A9: k < (m + 1) by A5, XXREAL_0: 2;

      then

       A10: k in ( Seg ( width G)) by A2, A4, FINSEQ_1: 1;

      

       A11: ( len ( Col (G,k))) = ( len G) by Def8;

      

       A12: ( len ( Col (N,k))) = ( len N) by Def8;

      

       A13: k <= m by A9, NAT_1: 13;

      then

       A14: k in ( Seg ( width N)) by A4, A6, FINSEQ_1: 1;

      now

        let j be Nat;

        

         A15: ( dom N) = ( Seg ( len N)) & ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

        assume 1 <= j & j <= ( len ( Col (N,k)));

        then

         A16: j in ( dom N) by A12, FINSEQ_3: 25;

        

        hence (( Col (N,k)) . j) = (N * (j,k)) by Def8

        .= (( Del (( Line (G,j)),i)) . k) by A1, A14, A7, A8, A16, A15, Th66

        .= (( Line (G,j)) . k) by A5, FINSEQ_3: 110

        .= (( Col (G,k)) . j) by A10, A8, A16, A15, Th42;

      end;

      hence thesis by A2, A4, A6, A9, A13, A12, A11, A8, FINSEQ_1: 1, FINSEQ_1: 14;

    end;

    theorem :: MATRIX_0:68

    

     Th68: i in ( Seg ( width G)) & ( width G) = (m + 1) & m > 0 & i <= k & k <= m implies ( Col (( DelCol (G,i)),k)) = ( Col (G,(k + 1))) & k in ( Seg ( width ( DelCol (G,i)))) & (k + 1) in ( Seg ( width G))

    proof

      set N = ( DelCol (G,i));

      assume that

       A1: i in ( Seg ( width G)) and

       A2: ( width G) = (m + 1) and

       A3: m > 0 and

       A4: i <= k and

       A5: k <= m;

      

       A6: ( len ( Col (N,k))) = ( len N) by Def8;

      

       A7: 1 < ( width G) by A2, A3, SEQM_3: 43;

      

       A8: ( len N) = ( len G) by Def13;

      

       A9: 1 <= (k + 1) & (k + 1) <= (m + 1) by A5, NAT_1: 11, XREAL_1: 6;

      then

       A10: (k + 1) in ( Seg ( width G)) by A2, FINSEQ_1: 1;

      1 <= i by A1, FINSEQ_1: 1;

      then

       A11: 1 <= k by A4, XXREAL_0: 2;

      

       A12: ( len ( Col (G,(k + 1)))) = ( len G) by Def8;

      

       A13: ( width N) = m by A1, A2, Th63;

      then

       A14: k in ( Seg ( width N)) by A5, A11, FINSEQ_1: 1;

      now

        let j be Nat;

        

         A15: ( dom N) = ( Seg ( len N)) & ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

        

         A16: ( len ( Line (G,j))) = (m + 1) & ( dom ( Line (G,j))) = ( Seg ( len ( Line (G,j)))) by A2, Def7, FINSEQ_1:def 3;

        assume 1 <= j & j <= ( len ( Col (N,k)));

        then

         A17: j in ( dom N) by A6, FINSEQ_3: 25;

        

        hence (( Col (N,k)) . j) = (N * (j,k)) by Def8

        .= (( Del (( Line (G,j)),i)) . k) by A1, A14, A7, A8, A17, A15, Th66

        .= (( Line (G,j)) . (k + 1)) by A1, A2, A4, A5, A16, FINSEQ_3: 111

        .= (( Col (G,(k + 1))) . j) by A10, A8, A17, A15, Th42;

      end;

      hence thesis by A2, A5, A13, A9, A11, A6, A12, A8, FINSEQ_1: 1, FINSEQ_1: 14;

    end;

    theorem :: MATRIX_0:69

    

     Th69: i in ( Seg ( width G)) & ( width G) = (m + 1) & m > 0 & n in ( dom G) & 1 <= k & k < i implies (( DelCol (G,i)) * (n,k)) = (G * (n,k)) & k in ( Seg ( width G))

    proof

      assume that

       A1: i in ( Seg ( width G)) and

       A2: ( width G) = (m + 1) & m > 0 and

       A3: n in ( dom G) and

       A4: 1 <= k & k < i;

      

       A5: ( len ( DelCol (G,i))) = ( len G) by Def13;

      

       A6: ( dom G) = ( Seg ( len G)) & ( Seg ( len ( DelCol (G,i)))) = ( dom ( DelCol (G,i))) by FINSEQ_1:def 3;

      ( Col (( DelCol (G,i)),k)) = ( Col (G,k)) by A1, A2, A4, Th67;

      

      hence (( DelCol (G,i)) * (n,k)) = (( Col (G,k)) . n) by A3, A6, A5, Def8

      .= (G * (n,k)) by A3, Def8;

      thus thesis by A1, A2, A4, Th67;

    end;

    theorem :: MATRIX_0:70

    

     Th70: i in ( Seg ( width G)) & ( width G) = (m + 1) & m > 0 & n in ( dom G) & i <= k & k <= m implies (( DelCol (G,i)) * (n,k)) = (G * (n,(k + 1))) & (k + 1) in ( Seg ( width G))

    proof

      assume that

       A1: i in ( Seg ( width G)) and

       A2: ( width G) = (m + 1) & m > 0 and

       A3: n in ( dom G) and

       A4: i <= k & k <= m;

      

       A5: ( len ( DelCol (G,i))) = ( len G) by Def13;

      

       A6: ( dom G) = ( Seg ( len G)) & ( Seg ( len ( DelCol (G,i)))) = ( dom ( DelCol (G,i))) by FINSEQ_1:def 3;

      ( Col (( DelCol (G,i)),k)) = ( Col (G,(k + 1))) by A1, A2, A4, Th68;

      

      hence (( DelCol (G,i)) * (n,k)) = (( Col (G,(k + 1))) . n) by A3, A6, A5, Def8

      .= (G * (n,(k + 1))) by A3, Def8;

      thus thesis by A1, A2, A4, Th68;

    end;

    theorem :: MATRIX_0:71

    ( width G) = (m + 1) & m > 0 & k in ( Seg m) implies ( Col (( DelCol (G,1)),k)) = ( Col (G,(k + 1))) & k in ( Seg ( width ( DelCol (G,1)))) & (k + 1) in ( Seg ( width G))

    proof

      assume that

       A1: ( width G) = (m + 1) and

       A2: m > 0 and

       A3: k in ( Seg m);

      1 <= ( width G) by A1, A2, SEQM_3: 43;

      then

       A4: 1 in ( Seg ( width G)) by FINSEQ_1: 1;

      1 <= k & k <= m by A3, FINSEQ_1: 1;

      hence thesis by A1, A4, Th68;

    end;

    theorem :: MATRIX_0:72

    ( width G) = (m + 1) & m > 0 & k in ( Seg m) & n in ( dom G) implies (( DelCol (G,1)) * (n,k)) = (G * (n,(k + 1))) & 1 in ( Seg ( width G))

    proof

      assume that

       A1: ( width G) = (m + 1) and

       A2: m > 0 and

       A3: k in ( Seg m) and

       A4: n in ( dom G);

      1 <= ( width G) by A1, A2, SEQM_3: 43;

      then

       A5: 1 in ( Seg ( width G)) by FINSEQ_1: 1;

      1 <= k & k <= m by A3, FINSEQ_1: 1;

      hence thesis by A1, A4, A5, Th70;

    end;

    theorem :: MATRIX_0:73

    ( width G) = (m + 1) & m > 0 & k in ( Seg m) implies ( Col (( DelCol (G,( width G))),k)) = ( Col (G,k)) & k in ( Seg ( width ( DelCol (G,( width G)))))

    proof

      assume that

       A1: ( width G) = (m + 1) and

       A2: m > 0 and

       A3: k in ( Seg m);

      k <= m by A3, FINSEQ_1: 1;

      then

       A4: k < ( width G) by A1, NAT_1: 13;

      1 <= ( width G) by A1, A2, SEQM_3: 43;

      then

       A5: ( width G) in ( Seg ( width G)) by FINSEQ_1: 1;

      1 <= k by A3, FINSEQ_1: 1;

      hence thesis by A1, A2, A5, A4, Th67;

    end;

    theorem :: MATRIX_0:74

    ( width G) = (m + 1) & m > 0 & k in ( Seg m) & n in ( dom G) implies k in ( Seg ( width G)) & (( DelCol (G,( width G))) * (n,k)) = (G * (n,k)) & ( width G) in ( Seg ( width G))

    proof

      assume that

       A1: ( width G) = (m + 1) and

       A2: m > 0 and

       A3: k in ( Seg m) and

       A4: n in ( dom G);

      k <= m by A3, FINSEQ_1: 1;

      then

       A5: k < ( width G) by A1, NAT_1: 13;

      1 <= ( width G) by A1, A2, SEQM_3: 43;

      then

       A6: ( width G) in ( Seg ( width G)) by FINSEQ_1: 1;

      1 <= k by A3, FINSEQ_1: 1;

      hence thesis by A1, A2, A4, A6, A5, Th69;

    end;

    reserve f for FinSequence of D,

G for Matrix of D;

    theorem :: MATRIX_0:75

    ( rng f) misses ( rng ( Col (G,i))) & (f /. n) in ( rng ( Line (G,m))) & n in ( dom f) & i in ( Seg ( width G)) & m in ( dom G) & ( width G) > 1 implies (f /. n) in ( rng ( Line (( DelCol (G,i)),m)))

    proof

      set D = ( DelCol (G,i));

      assume that

       A1: ( rng f) misses ( rng ( Col (G,i))) and

       A2: (f /. n) in ( rng ( Line (G,m))) and

       A3: n in ( dom f) and

       A4: i in ( Seg ( width G)) and

       A5: m in ( dom G) and

       A6: ( width G) > 1;

      

       A7: ( len ( Line (D,m))) = ( width D) & ( dom ( Line (D,m))) = ( Seg ( len ( Line (D,m)))) by Def7, FINSEQ_1:def 3;

      consider j be Nat such that

       A8: j in ( dom ( Line (G,m))) and

       A9: (f /. n) = (( Line (G,m)) . j) by A2, FINSEQ_2: 10;

      reconsider j as Nat;

      

       A10: ( len ( Line (G,m))) = ( width G) by Def7;

      then

       A11: j <= ( width G) by A8, FINSEQ_3: 25;

      

       A12: ( dom ( Line (G,m))) = ( Seg ( len ( Line (G,m)))) by FINSEQ_1:def 3;

      then

       A13: 1 <= i by A4, A10, FINSEQ_3: 25;

      

       A14: (f /. n) = (G * (m,j)) by A8, A9, A12, A10, Def7;

      

       A15: i <= ( width G) by A4, A12, A10, FINSEQ_3: 25;

      

       A16: 1 <= j by A8, FINSEQ_3: 25;

      consider M be Nat such that

       A17: ( width G) = (M + 1) and

       A18: M > 0 by A6, SEQM_3: 43;

      

       A19: ( width D) = M by A4, A17, Th63;

      i <> j by A1, A3, A5, A14, Th43;

      per cases by XXREAL_0: 1;

        suppose

         A20: j < i;

        then j < ( width G) by A15, XXREAL_0: 2;

        then j <= M by A17, NAT_1: 13;

        then

         A21: j in ( Seg ( width D)) by A16, A19, FINSEQ_1: 1;

        (f /. n) = (D * (m,j)) by A4, A5, A14, A16, A17, A18, A20, Th69;

        then (( Line (D,m)) . j) = (f /. n) by A21, Def7;

        hence thesis by A7, A21, FUNCT_1:def 3;

      end;

        suppose

         A22: i < j;

        reconsider l = (j - 1) as Element of NAT by A16, INT_1: 5;

        

         A23: l <= M by A11, A17, XREAL_1: 20;

        (i + 1) <= j by A22, NAT_1: 13;

        then

         A24: i <= l by XREAL_1: 19;

        then 1 <= l by A13, XXREAL_0: 2;

        then

         A25: l in ( Seg ( width D)) by A19, A23, FINSEQ_1: 1;

        (l + 1) = j;

        then (f /. n) = (D * (m,l)) by A4, A5, A14, A13, A17, A24, A23, Th70;

        then (( Line (D,m)) . l) = (f /. n) by A25, Def7;

        hence thesis by A7, A25, FUNCT_1:def 3;

      end;

    end;