matrlin.miz



    begin

    reserve k,t,i,j,m,n for Nat,

x,y,y1,y2 for object,

D for non empty set;

    definition

      let D be non empty set;

      let k;

      let M be Matrix of D;

      :: original: Del

      redefine

      func Del (M,k) -> Matrix of D ;

      coherence

      proof

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

        proof

          consider n such that

           A1: for x st x in ( rng M) holds ex p be FinSequence of D st x = p & ( len p) = n by MATRIX_0: 9;

          take n;

          let x such that

           A2: x in ( rng ( Del (M,k)));

          ( Del (M,k)) is FinSequence of (D * ) by FINSEQ_3: 105;

          then ( rng ( Del (M,k))) c= (D * ) by FINSEQ_1:def 4;

          then

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

          take p;

          ( rng ( Del (M,k))) c= ( rng M) by FINSEQ_3: 106;

          then ex p1 be FinSequence of D st x = p1 & ( len p1) = n by A1, A2;

          hence thesis;

        end;

        hence thesis by MATRIX_0: 9;

      end;

    end

    ::$Canceled

    

     Th1: for M be FinSequence st ( len M) = (n + 1) holds ( len ( Del (M,(n + 1)))) = n by PRE_POLY: 12;

    theorem :: MATRLIN:2

    

     Th2: for M be Matrix of (n + 1), m, D holds for M1 be Matrix of D holds (n > 0 implies ( width M) = ( width ( Del (M,(n + 1))))) & (M1 = <*(M . (n + 1))*> implies ( width M) = ( width M1))

    proof

      let M be Matrix of (n + 1), m, D;

      let M1 be Matrix of D;

      

       A1: ( len M) = (n + 1) by MATRIX_0:def 2;

      then (n + 1) in ( Seg ( len M)) by FINSEQ_1: 4;

      then (n + 1) in ( dom M) by FINSEQ_1:def 3;

      then

       A2: (M . (n + 1)) = ( Line (M,(n + 1))) by MATRIX_0: 60;

      now

        assume

         A3: n > 0 ;

        ( len ( Del (M,(n + 1)))) = n by A1, Th1;

        then

        consider s be FinSequence such that

         A4: s in ( rng ( Del (M,(n + 1)))) and

         A5: ( len s) = ( width ( Del (M,(n + 1)))) by A3, MATRIX_0:def 3;

        consider n1 be Nat such that

         A6: for x st x in ( rng M) holds ex p be FinSequence of D st x = p & ( len p) = n1 by MATRIX_0: 9;

        consider s1 be FinSequence such that

         A7: s1 in ( rng M) and

         A8: ( len s1) = ( width M) by A1, MATRIX_0:def 3;

        

         A9: ex p2 be FinSequence of D st s1 = p2 & ( len p2) = n1 by A7, A6;

        ( rng ( Del (M,(n + 1)))) c= ( rng M) by FINSEQ_3: 106;

        then ex p1 be FinSequence of D st s = p1 & ( len p1) = n1 by A4, A6;

        hence ( width M) = ( width ( Del (M,(n + 1)))) by A5, A8, A9;

      end;

      hence n > 0 implies ( width M) = ( width ( Del (M,(n + 1))));

      assume M1 = <*(M . (n + 1))*>;

      then

      reconsider M2 = M1 as Matrix of 1, ( len ( Line (M,(n + 1)))), D by A2, MATRIX_0: 11;

      

      thus ( width M) = ( len ( Line (M,(n + 1)))) by MATRIX_0:def 7

      .= ( width M2) by MATRIX_0: 23

      .= ( width M1);

    end;

    theorem :: MATRLIN:3

    

     Th3: for M be Matrix of (n + 1), m, D holds ( Del (M,(n + 1))) is Matrix of n, m, D

    proof

      let M be Matrix of (n + 1), m, D;

      

       A1: ( len M) = (n + 1) by MATRIX_0:def 2;

      then

       A2: ( len ( Del (M,(n + 1)))) = n by Th1;

      per cases ;

        suppose

         A3: n = 0 ;

        then ( Del (M,(n + 1))) = {} by A2;

        hence thesis by A3, MATRIX_0: 13;

      end;

        suppose

         A4: n > 0 ;

        ( width M) = m by A1, MATRIX_0: 20;

        then ( width ( Del (M,(n + 1)))) = m by A4, Th2;

        hence thesis by A2, A4, MATRIX_0: 20;

      end;

    end;

    ::$Canceled

    

     Th4: for M be FinSequence st M <> {} holds M = (( Del (M,( len M))) ^ <*(M . ( len M))*>) by PRE_POLY: 13;

    definition

      let D;

      let P be FinSequence of D;

      :: original: <*

      redefine

      func <*P*> -> Matrix of 1, ( len P), D ;

      coherence by MATRIX_0: 11;

    end

    begin

    begin

    reserve K for Field,

V for VectSp of K,

a for Element of K,

W for Element of V;

    reserve KL1,KL2,KL3 for Linear_Combination of V,

X for Subset of V;

    theorem :: MATRLIN:5

    

     Th5: X is linearly-independent & ( Carrier KL1) c= X & ( Carrier KL2) c= X & ( Sum KL1) = ( Sum KL2) implies KL1 = KL2

    proof

      assume that

       A1: X is linearly-independent and

       A2: ( Carrier KL1) c= X & ( Carrier KL2) c= X and

       A3: ( Sum KL1) = ( Sum KL2);

      (( Sum KL1) - ( Sum KL2)) = ( 0. V) by A3, VECTSP_1: 19;

      then

       A4: (KL1 - KL2) is Linear_Combination of ( Carrier (KL1 - KL2)) & ( Sum (KL1 - KL2)) = ( 0. V) by VECTSP_6: 7, VECTSP_6: 47;

      

       A5: ( Carrier (KL1 - KL2)) c= (( Carrier KL1) \/ ( Carrier KL2)) by VECTSP_6: 41;

      (( Carrier KL1) \/ ( Carrier KL2)) c= X by A2, XBOOLE_1: 8;

      then

       A6: ( Carrier (KL1 - KL2)) is linearly-independent by A1, A5, VECTSP_7: 1, XBOOLE_1: 1;

      now

        let v be Vector of V;

         not v in ( Carrier (KL1 - KL2)) by A6, A4, VECTSP_7:def 1;

        then ((KL1 - KL2) . v) = ( 0. K) by VECTSP_6: 2;

        then ((KL1 . v) - (KL2 . v)) = ( 0. K) by VECTSP_6: 40;

        hence (KL1 . v) = (KL2 . v) by RLVECT_1: 21;

      end;

      hence thesis by VECTSP_6:def 7;

    end;

    theorem :: MATRLIN:6

    

     Th6: X is linearly-independent & ( Carrier KL1) c= X & ( Carrier KL2) c= X & ( Carrier KL3) c= X & ( Sum KL1) = (( Sum KL2) + ( Sum KL3)) implies KL1 = (KL2 + KL3)

    proof

      assume that

       A1: X is linearly-independent & ( Carrier KL1) c= X and

       A2: ( Carrier KL2) c= X & ( Carrier KL3) c= X and

       A3: ( Sum KL1) = (( Sum KL2) + ( Sum KL3));

      ( Carrier (KL2 + KL3)) c= (( Carrier KL2) \/ ( Carrier KL3)) & (( Carrier KL2) \/ ( Carrier KL3)) c= X by A2, VECTSP_6: 23, XBOOLE_1: 8;

      then

       A4: ( Carrier (KL2 + KL3)) c= X;

      ( Sum KL1) = ( Sum (KL2 + KL3)) by A3, VECTSP_6: 44;

      hence thesis by A1, A4, Th5;

    end;

    theorem :: MATRLIN:7

    

     Th7: X is linearly-independent & ( Carrier KL1) c= X & ( Carrier KL2) c= X & a <> ( 0. K) & ( Sum KL1) = (a * ( Sum KL2)) implies KL1 = (a * KL2)

    proof

      assume that

       A1: X is linearly-independent & ( Carrier KL1) c= X and

       A2: ( Carrier KL2) c= X & a <> ( 0. K) & ( Sum KL1) = (a * ( Sum KL2));

      ( Carrier (a * KL2)) c= X & ( Sum KL1) = ( Sum (a * KL2)) by A2, VECTSP_6: 29, VECTSP_6: 45;

      hence thesis by A1, Th5;

    end;

    theorem :: MATRLIN:8

    

     Th8: for b2 be Basis of V holds ex KL be Linear_Combination of V st W = ( Sum KL) & ( Carrier KL) c= b2

    proof

      let b2 be Basis of V;

      W in the ModuleStr of V by RLVECT_1: 1;

      then W in ( Lin b2) by VECTSP_7:def 3;

      then

      consider KL1 be Linear_Combination of b2 such that

       A1: W = ( Sum KL1) by VECTSP_7: 7;

      take KL = KL1;

      thus W = ( Sum KL) by A1;

      thus thesis by VECTSP_6:def 4;

    end;

    definition

      let K be Field;

      let V be VectSp of K;

      :: MATRLIN:def1

      attr V is finite-dimensional means

      : Def1: ex A be finite Subset of V st A is Basis of V;

    end

    registration

      let K be Field;

      cluster strict finite-dimensional for VectSp of K;

      existence

      proof

        set V = the VectSp of K;

        take ( (0). V);

        thus ( (0). V) is strict;

        take A = ( {} the carrier of ( (0). V));

        ( Lin A) = ( (0). ( (0). V)) by VECTSP_7: 9;

        then ( Lin A) = the ModuleStr of ( (0). V) by VECTSP_4: 36;

        hence thesis by VECTSP_7:def 3;

      end;

    end

    definition

      let K be Field;

      let V be finite-dimensional VectSp of K;

      :: MATRLIN:def2

      mode OrdBasis of V -> FinSequence of V means

      : Def2: it is one-to-one & ( rng it ) is Basis of V;

      existence

      proof

        consider A be finite Subset of V such that

         A1: A is Basis of V by Def1;

        consider p be FinSequence such that

         A2: ( rng p) = A and

         A3: p is one-to-one by FINSEQ_4: 58;

        reconsider p as FinSequence of V by A2, FINSEQ_1:def 4;

        take f = p;

        thus f is one-to-one by A3;

        thus thesis by A1, A2;

      end;

    end

    reserve s for FinSequence,

V1,V2,V3 for finite-dimensional VectSp of K,

f,f1,f2 for Function of V1, V2,

g for Function of V2, V3,

b1 for OrdBasis of V1,

b2 for OrdBasis of V2,

b3 for OrdBasis of V3,

v1,v2 for Vector of V2,

v,w for Element of V1;

    reserve p2,F for FinSequence of V1,

p1,d for FinSequence of K,

KL for Linear_Combination of V1;

    definition

      let K be non empty doubleLoopStr;

      let V1,V2 be non empty ModuleStr over K;

      let f1,f2 be Function of V1, V2;

      :: MATRLIN:def3

      func f1 + f2 -> Function of V1, V2 means

      : Def3: for v be Element of V1 holds (it . v) = ((f1 . v) + (f2 . v));

      existence

      proof

        deffunc F( Element of V1) = ((f1 . $1) + (f2 . $1));

        consider F be Function of V1, V2 such that

         A1: for v be Element of V1 holds (F . v) = F(v) from FUNCT_2:sch 4;

        reconsider F as Function of V1, V2;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Function of V1, V2 such that

         A2: for v be Element of V1 holds (F . v) = ((f1 . v) + (f2 . v)) and

         A3: for v be Element of V1 holds (G . v) = ((f1 . v) + (f2 . v));

        now

          let v be Element of V1;

          

          thus (F . v) = ((f1 . v) + (f2 . v)) by A2

          .= (G . v) by A3;

        end;

        hence F = G by FUNCT_2: 63;

      end;

    end

    definition

      let K be non empty doubleLoopStr;

      let V1,V2 be non empty ModuleStr over K;

      let f be Function of V1, V2;

      let a be Element of K;

      :: MATRLIN:def4

      func a * f -> Function of V1, V2 means

      : Def4: for v be Element of V1 holds (it . v) = (a * (f . v));

      existence

      proof

        deffunc F( Element of V1) = (a * (f . $1));

        consider F be Function of V1, V2 such that

         A1: for v be Element of V1 holds (F . v) = F(v) from FUNCT_2:sch 4;

        reconsider F as Function of V1, V2;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Function of V1, V2 such that

         A2: for v be Element of V1 holds (F . v) = (a * (f . v)) and

         A3: for v be Element of V1 holds (G . v) = (a * (f . v));

        now

          let v be Element of V1;

          

          thus (F . v) = (a * (f . v)) by A2

          .= (G . v) by A3;

        end;

        hence F = G by FUNCT_2: 63;

      end;

    end

    theorem :: MATRLIN:9

    

     Th9: for a be Element of V1 holds for F be FinSequence of V1 holds for G be FinSequence of K st ( len F) = ( len G) & for k holds for v be Element of K st k in ( dom F) & v = (G . k) holds (F . k) = (v * a) holds ( Sum F) = (( Sum G) * a)

    proof

      let a be Element of V1;

      let F be FinSequence of V1;

      let G be FinSequence of K;

      defpred P[ Nat] means for H be FinSequence of V1, I be FinSequence of K st ( len H) = ( len I) & ( len H) = $1 & (for k holds for v be Element of K st k in ( dom H) & v = (I . k) holds (H . k) = (v * a)) holds ( Sum H) = (( Sum I) * a);

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A2: for H be FinSequence of V1, I be FinSequence of K st ( len H) = ( len I) & ( len H) = n & (for k holds for v be Element of K st k in ( dom H) & v = (I . k) holds (H . k) = (v * a)) holds ( Sum H) = (( Sum I) * a);

        let H be FinSequence of V1, I be FinSequence of K;

        assume that

         A3: ( len H) = ( len I) and

         A4: ( len H) = (n + 1) and

         A5: for k holds for v be Element of K st k in ( dom H) & v = (I . k) holds (H . k) = (v * a);

        reconsider q = (I | ( Seg n)) as FinSequence of K by FINSEQ_1: 18;

        reconsider p = (H | ( Seg n)) as FinSequence of V1 by FINSEQ_1: 18;

        

         A6: n <= (n + 1) by NAT_1: 12;

        then

         A7: ( len p) = n by A4, FINSEQ_1: 17;

        

         A8: ( dom p) = ( Seg n) by A4, A6, FINSEQ_1: 17;

        

         A9: ( len q) = n by A3, A4, A6, FINSEQ_1: 17;

        

         A10: ( dom q) = ( Seg n) by A3, A4, A6, FINSEQ_1: 17;

         A11:

        now

          ( len p) <= ( len H) by A4, A6, FINSEQ_1: 17;

          then

           A12: ( dom p) c= ( dom H) by FINSEQ_3: 30;

          let k;

          let v be Element of K;

          assume that

           A13: k in ( dom p) and

           A14: v = (q . k);

          (I . k) = (q . k) by A8, A10, A13, FUNCT_1: 47;

          then (H . k) = (v * a) by A5, A13, A14, A12;

          hence (p . k) = (v * a) by A13, FUNCT_1: 47;

        end;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then

         A15: (n + 1) in ( dom H) by A4, FINSEQ_1:def 3;

        then

        reconsider v1 = (H . (n + 1)) as Element of V1 by FINSEQ_2: 11;

        ( dom H) = ( dom I) by A3, FINSEQ_3: 29;

        then

        reconsider v2 = (I . (n + 1)) as Element of K by A15, FINSEQ_2: 11;

        

         A16: v1 = (v2 * a) by A5, A15;

        

        thus ( Sum H) = (( Sum p) + v1) by A4, A7, A8, RLVECT_1: 38

        .= ((( Sum q) * a) + (v2 * a)) by A2, A7, A9, A11, A16

        .= ((( Sum q) + v2) * a) by VECTSP_1:def 15

        .= (( Sum I) * a) by A3, A4, A9, A10, RLVECT_1: 38;

      end;

      

       A17: P[ 0 ]

      proof

        let H be FinSequence of V1, I be FinSequence of K;

        assume that

         A18: ( len H) = ( len I) and

         A19: ( len H) = 0 and for k holds for v be Element of K st k in ( dom H) & v = (I . k) holds (H . k) = (v * a);

        H = ( <*> the carrier of V1) by A19;

        then

         A20: ( Sum H) = ( 0. V1) by RLVECT_1: 43;

        I = ( <*> the carrier of K) by A18, A19;

        then ( Sum I) = ( 0. K) by RLVECT_1: 43;

        hence thesis by A20, VECTSP_1: 14;

      end;

      for n holds P[n] from NAT_1:sch 2( A17, A1);

      hence thesis;

    end;

    theorem :: MATRLIN:10

    

     Th10: for a be Element of V1 holds for F be FinSequence of K holds for G be FinSequence of V1 st ( len F) = ( len G) & for k st k in ( dom F) holds (G . k) = ((F /. k) * a) holds ( Sum G) = (( Sum F) * a)

    proof

      let a be Element of V1;

      let F be FinSequence of K;

      let G be FinSequence of V1;

      assume that

       A1: ( len F) = ( len G) and

       A2: for k st k in ( dom F) holds (G . k) = ((F /. k) * a);

      now

        let k;

        let v be Element of K;

        assume that

         A3: k in ( dom G) and

         A4: v = (F . k);

        

         A5: k in ( dom F) by A1, A3, FINSEQ_3: 29;

        then v = (F /. k) by A4, PARTFUN1:def 6;

        hence (G . k) = (v * a) by A2, A5;

      end;

      hence thesis by A1, Th9;

    end;

    theorem :: MATRLIN:11

    

     Th11: for V1 be add-associative right_zeroed right_complementable non empty addLoopStr holds for F be FinSequence of V1 st for k st k in ( dom F) holds (F /. k) = ( 0. V1) holds ( Sum F) = ( 0. V1)

    proof

      let V1 be add-associative right_zeroed right_complementable non empty addLoopStr;

      let F be FinSequence of V1;

      assume

       A1: for k st k in ( dom F) holds (F /. k) = ( 0. V1);

      defpred P[ FinSequence of V1] means ((for k st k in ( dom $1) holds ($1 /. k) = ( 0. V1)) implies ( Sum $1) = ( 0. V1));

      

       A2: for p be FinSequence of V1, x be Element of V1 holds P[p] implies P[(p ^ <*x*>)]

      proof

        let p be FinSequence of V1;

        let x be Element of V1;

        assume

         A3: (for k st k in ( dom p) holds (p /. k) = ( 0. V1)) implies ( Sum p) = ( 0. V1);

        

         A4: (( len p) + 1) in ( Seg (( len p) + 1)) by FINSEQ_1: 4;

        assume

         A5: for k st k in ( dom (p ^ <*x*>)) holds ((p ^ <*x*>) /. k) = ( 0. V1);

        

         A6: for k st k in ( dom p) holds (p /. k) = ( 0. V1)

        proof

          

           A7: ( dom p) c= ( dom (p ^ <*x*>)) by FINSEQ_1: 26;

          let k such that

           A8: k in ( dom p);

          reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

          

          thus (p /. k) = (p . k) by A8, PARTFUN1:def 6

          .= ((p ^ <*x*>) . k1) by A8, FINSEQ_1:def 7

          .= ((p ^ <*x*>) /. k) by A8, A7, PARTFUN1:def 6

          .= ( 0. V1) by A5, A8, A7;

        end;

        ( len (p ^ <*x*>)) = (( len p) + ( len <*x*>)) by FINSEQ_1: 22

        .= (( len p) + 1) by FINSEQ_1: 39;

        then

         A9: (( len p) + 1) in ( dom (p ^ <*x*>)) by A4, FINSEQ_1:def 3;

        

         A10: x = ((p ^ <*x*>) . (( len p) + 1)) by FINSEQ_1: 42;

        

        thus ( Sum (p ^ <*x*>)) = (( Sum p) + ( Sum <*x*>)) by RLVECT_1: 41

        .= (( Sum p) + x) by RLVECT_1: 44

        .= (( Sum p) + ((p ^ <*x*>) /. (( len p) + 1))) by A9, A10, PARTFUN1:def 6

        .= (( 0. V1) + ( 0. V1)) by A3, A5, A6, A9

        .= ( 0. V1) by RLVECT_1:def 4;

      end;

      

       A11: P[( <*> the carrier of V1)] by RLVECT_1: 43;

      for p be FinSequence of V1 holds P[p] from FINSEQ_2:sch 2( A11, A2);

      hence thesis by A1;

    end;

    definition

      let K, V1, p1, p2;

      :: MATRLIN:def5

      func lmlt (p1,p2) -> FinSequence of V1 equals (the lmult of V1 .: (p1,p2));

      coherence ;

    end

    theorem :: MATRLIN:12

    

     Th12: ( dom p1) = ( dom p2) implies ( dom ( lmlt (p1,p2))) = ( dom p1)

    proof

      assume

       A1: ( dom p1) = ( dom p2);

      ( rng p1) c= the carrier of K & ( rng p2) c= the carrier of V1 by FINSEQ_1:def 4;

      then

       A2: [:( rng p1), ( rng p2):] c= [:the carrier of K, the carrier of V1:] by ZFMISC_1: 96;

      ( rng <:p1, p2:>) c= [:( rng p1), ( rng p2):] & [:the carrier of K, the carrier of V1:] = ( dom the lmult of V1) by FUNCT_2:def 1, FUNCT_3: 51;

      

      hence ( dom ( lmlt (p1,p2))) = ( dom <:p1, p2:>) by A2, RELAT_1: 27, XBOOLE_1: 1

      .= (( dom p1) /\ ( dom p2)) by FUNCT_3:def 7

      .= ( dom p1) by A1;

    end;

    definition

      let V1 be non empty addLoopStr, M be FinSequence of (the carrier of V1 * );

      :: MATRLIN:def6

      func Sum M -> FinSequence of V1 means

      : Def6: ( len it ) = ( len M) & for k st k in ( dom it ) holds (it /. k) = ( Sum (M /. k));

      existence

      proof

        deffunc F( Nat) = ( Sum (M /. $1));

        consider F be FinSequence of V1 such that

         A1: ( len F) = ( len M) & for k be Nat st k in ( dom F) holds (F . k) = F(k) from FINSEQ_2:sch 1;

        take F;

        thus ( len F) = ( len M) by A1;

        hereby

          let k;

          assume

           A2: k in ( dom F);

          

          hence (F /. k) = (F . k) by PARTFUN1:def 6

          .= ( Sum (M /. k)) by A1, A2;

        end;

      end;

      uniqueness

      proof

        let F1,F2 be FinSequence of V1 such that

         A3: ( len F1) = ( len M) and

         A4: for k st k in ( dom F1) holds (F1 /. k) = ( Sum (M /. k)) and

         A5: ( len F2) = ( len M) and

         A6: for k st k in ( dom F2) holds (F2 /. k) = ( Sum (M /. k));

        

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

        now

          let k be Nat;

          assume

           A8: k in ( dom F1);

          then

           A9: k in ( dom F2) by A3, A5, A7, FINSEQ_1:def 3;

          

          thus (F1 . k) = (F1 /. k) by A8, PARTFUN1:def 6

          .= ( Sum (M /. k)) by A4, A8

          .= (F2 /. k) by A6, A9

          .= (F2 . k) by A9, PARTFUN1:def 6;

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

    end

    theorem :: MATRLIN:13

    

     Th13: for M be Matrix of the carrier of V1 st ( len M) = 0 holds ( Sum ( Sum M)) = ( 0. V1)

    proof

      let M be Matrix of the carrier of V1;

      assume ( len M) = 0 ;

      then ( len ( Sum M)) = 0 by Def6;

      then ( Sum M) = ( <*> the carrier of V1);

      hence thesis by RLVECT_1: 43;

    end;

    theorem :: MATRLIN:14

    

     Th14: for M be Matrix of (m + 1), 0 , the carrier of V1 holds ( Sum ( Sum M)) = ( 0. V1)

    proof

      let M be Matrix of (m + 1), 0 , the carrier of V1;

      for k st k in ( dom ( Sum M)) holds (( Sum M) /. k) = ( 0. V1)

      proof

        let k such that

         A1: k in ( dom ( Sum M));

        reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

        ( len M) = ( len ( Sum M)) by Def6;

        then ( dom M) = ( dom ( Sum M)) by FINSEQ_3: 29;

        then (M /. k1) in ( rng M) by A1, PARTFUN2: 2;

        then ( len (M /. k)) = 0 by MATRIX_0:def 2;

        then

         A2: (M /. k) = ( <*> the carrier of V1);

        

        thus (( Sum M) /. k) = ( Sum (M /. k)) by A1, Def6

        .= ( 0. V1) by A2, RLVECT_1: 43;

      end;

      hence thesis by Th11;

    end;

    theorem :: MATRLIN:15

    

     Th15: for x be Element of D holds <* <*x*>*> = ( <* <*x*>*> @ )

    proof

      let x be Element of D;

      set P = <* <*x*>*>, R = ( <* <*x*>*> @ );

      

       A1: ( len P) = 1 by FINSEQ_1: 40;

      

      then

       A2: ( width P) = ( len <*x*>) by MATRIX_0: 20

      .= 1 by FINSEQ_1: 40;

      then

       A3: ( len R) = 1 by MATRIX_0: 54;

       A4:

      now

        let i, j;

        assume

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

        then

         A6: [i, j] in [:( dom P), ( Seg 1):] by A2, MATRIX_0:def 4;

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

        then i in ( Seg 1) by A1, FINSEQ_1:def 3;

        then

         A7: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

        j in ( Seg 1) by A6, ZFMISC_1: 87;

        then j = 1 by FINSEQ_1: 2, TARSKI:def 1;

        hence (P * (i,j)) = (R * (i,j)) by A5, A7, MATRIX_0:def 6;

      end;

      ( width R) = 1 by A1, A2, MATRIX_0: 54;

      hence thesis by A1, A2, A3, A4, MATRIX_0: 21;

    end;

    theorem :: MATRLIN:16

    

     Th16: for V1,V2 be VectSp of K, f be Function of V1, V2, p be FinSequence of V1 st f is additive homogeneous holds (f . ( Sum p)) = ( Sum (f * p))

    proof

      let V1,V2 be VectSp of K, f be Function of V1, V2;

      let p be FinSequence of V1;

      defpred P[ FinSequence of V1] means (f . ( Sum $1)) = ( Sum (f * $1));

      assume

       A1: f is additive homogeneous;

      

       A2: for p be FinSequence of V1 holds for w be Element of V1 st P[p] holds P[(p ^ <*w*>)]

      proof

        let p be FinSequence of V1;

        let w be Element of V1 such that

         A3: (f . ( Sum p)) = ( Sum (f * p));

        

        thus (f . ( Sum (p ^ <*w*>))) = (f . (( Sum p) + ( Sum <*w*>))) by RLVECT_1: 41

        .= (( Sum (f * p)) + (f . ( Sum <*w*>))) by A1, A3, VECTSP_1:def 20

        .= (( Sum (f * p)) + (f . w)) by RLVECT_1: 44

        .= (( Sum (f * p)) + ( Sum <*(f . w)*>)) by RLVECT_1: 44

        .= ( Sum ((f * p) ^ <*(f . w)*>)) by RLVECT_1: 41

        .= ( Sum (f * (p ^ <*w*>))) by FINSEQOP: 8;

      end;

      (f . ( Sum ( <*> the carrier of V1))) = (f . ( 0. V1)) by RLVECT_1: 43

      .= (f . (( 0. K) * ( 0. V1))) by VECTSP_1: 14

      .= (( 0. K) * (f . ( 0. V1))) by A1, MOD_2:def 2

      .= ( 0. V2) by VECTSP_1: 14

      .= ( Sum ( <*> the carrier of V2)) by RLVECT_1: 43

      .= ( Sum (f * ( <*> the carrier of V1)));

      then

       A4: P[( <*> the carrier of V1)];

      for p be FinSequence of V1 holds P[p] from FINSEQ_2:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: MATRLIN:17

    

     Th17: for a be FinSequence of K, p be FinSequence of V1 st ( len p) = ( len a) holds f is additive homogeneous implies (f * ( lmlt (a,p))) = ( lmlt (a,(f * p)))

    proof

      let a be FinSequence of K, p be FinSequence of V1;

      assume ( len p) = ( len a);

      then

       A1: ( dom p) = ( dom a) by FINSEQ_3: 29;

      ( dom f) = the carrier of V1 by FUNCT_2:def 1;

      then ( rng p) c= ( dom f) by FINSEQ_1:def 4;

      then

       A2: ( dom p) = ( dom (f * p)) by RELAT_1: 27;

      assume

       A3: f is additive homogeneous;

       A4:

      now

        set P = (f * p);

        let k be Nat;

        assume

         A5: k in ( dom (f * ( lmlt (a,p))));

        

         A6: ( dom (f * ( lmlt (a,p)))) c= ( dom ( lmlt (a,p))) by RELAT_1: 25;

        then k in ( dom ( lmlt (a,p))) by A5;

        then

         A7: k in ( dom p) by A1, Th12;

        then

         A8: (p /. k) = (p . k) by PARTFUN1:def 6;

        

         A9: k in ( dom ( lmlt (a,(f * p)))) by A1, A2, A7, Th12;

        

         A10: (a /. k) = (a . k) by A1, A7, PARTFUN1:def 6;

        

         A11: (P /. k) = ((f * p) . k) by A2, A7, PARTFUN1:def 6;

        

        thus ((f * ( lmlt (a,p))) . k) = (f . (( lmlt (a,p)) . k)) by A5, FUNCT_1: 12

        .= (f . (the lmult of V1 . ((a . k),(p . k)))) by A5, A6, FUNCOP_1: 22

        .= (f . ((a /. k) * (p /. k))) by A10, A8, VECTSP_1:def 12

        .= ((a /. k) * (f . (p /. k))) by A3, MOD_2:def 2

        .= ((a /. k) * (P /. k)) by A7, A8, A11, FUNCT_1: 13

        .= (the lmult of V2 . ((a . k),((f * p) . k))) by A10, A11, VECTSP_1:def 12

        .= (( lmlt (a,(f * p))) . k) by A9, FUNCOP_1: 22;

      end;

      ( dom ( lmlt (a,p))) = ( dom p) by A1, Th12

      .= ( dom ( lmlt (a,(f * p)))) by A1, A2, Th12;

      then ( len ( lmlt (a,p))) = ( len ( lmlt (a,(f * p)))) by FINSEQ_3: 29;

      then ( len (f * ( lmlt (a,p)))) = ( len ( lmlt (a,(f * p)))) by FINSEQ_2: 33;

      hence thesis by A4, FINSEQ_2: 9;

    end;

    theorem :: MATRLIN:18

    

     Th18: for a be FinSequence of K st ( len a) = ( len b2) & g is additive homogeneous holds (g . ( Sum ( lmlt (a,b2)))) = ( Sum ( lmlt (a,(g * b2))))

    proof

      let a be FinSequence of K such that

       A1: ( len a) = ( len b2) and

       A2: g is additive homogeneous;

      

      thus (g . ( Sum ( lmlt (a,b2)))) = ( Sum (g * ( lmlt (a,b2)))) by A2, Th16

      .= ( Sum ( lmlt (a,(g * b2)))) by A1, A2, Th17;

    end;

    theorem :: MATRLIN:19

    

     Th19: for F,F1 be FinSequence of V1, KL be Linear_Combination of V1, p be Permutation of ( dom F) st F1 = (F * p) holds (KL (#) F1) = ((KL (#) F) * p)

    proof

      let F,F1 be FinSequence of V1;

      let KL be Linear_Combination of V1;

      let p be Permutation of ( dom F) such that

       A1: F1 = (F * p);

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

      then ( dom F) = ( Seg ( len (KL (#) F))) by VECTSP_6:def 5;

      then

       A2: ( dom F) = ( dom (KL (#) F)) by FINSEQ_1:def 3;

      then

      reconsider F2 = ((KL (#) F) * p) as FinSequence of V1 by FINSEQ_2: 47;

      ( len (KL (#) F1)) = ( len F1) by VECTSP_6:def 5

      .= ( len F) by A1, FINSEQ_2: 44

      .= ( len (KL (#) F)) by VECTSP_6:def 5

      .= ( len F2) by A2, FINSEQ_2: 44;

      then

       A3: ( dom (KL (#) F1)) = ( dom ((KL (#) F) * p)) by FINSEQ_3: 29;

      ( len (KL (#) F1)) = ( len F1) by VECTSP_6:def 5;

      then

       A4: ( dom (KL (#) F1)) = ( dom F1) by FINSEQ_3: 29;

      now

        let k be Nat;

        reconsider k0 = k as Element of NAT by ORDINAL1:def 12;

        assume

         A5: k in ( dom (KL (#) F1));

        then k in ( dom p) by A3, FUNCT_1: 11;

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

        then

         A6: (p . k) in ( dom F) by FUNCT_2:def 3;

        then

        reconsider k1 = (p . k0) as Element of NAT by FINSEQ_3: 23;

        (F1 /. k) = (F1 . k) by A4, A5, PARTFUN1:def 6

        .= (F . (p . k)) by A1, A4, A5, FUNCT_1: 12

        .= (F /. (p . k)) by A6, PARTFUN1:def 6;

        

        hence ((KL (#) F1) . k) = ((KL . (F /. k1)) * (F /. k1)) by A5, VECTSP_6:def 5

        .= ((KL (#) F) . k1) by A2, A6, VECTSP_6:def 5

        .= (F2 . k) by A3, A5, FUNCT_1: 12;

      end;

      hence thesis by A3, FINSEQ_1: 13;

    end;

    theorem :: MATRLIN:20

    

     Th20: F is one-to-one & ( Carrier KL) c= ( rng F) implies ( Sum (KL (#) F)) = ( Sum KL)

    proof

      assume

       A1: F is one-to-one;

      assume

       A2: ( Carrier KL) c= ( rng F);

      then

      reconsider A = ( Carrier KL) as Subset of ( rng F);

      consider p1 be Permutation of ( dom F) such that

       A3: ((F - (A ` )) ^ (F - A)) = (F * p1) by FINSEQ_3: 115;

      reconsider G1 = (F - (A ` )), G2 = (F - A) as FinSequence of V1 by FINSEQ_3: 86;

      

       A4: G1 is one-to-one by A1, FINSEQ_3: 87;

      ( len (KL (#) F)) = ( len F) by VECTSP_6:def 5;

      then ( dom (KL (#) F)) = ( dom F) by FINSEQ_3: 29;

      then

      reconsider p1 as Permutation of ( dom (KL (#) F));

      

       A5: ( rng G1) = (( rng F) \ (A ` )) by FINSEQ_3: 65

      .= (( rng F) \ (( rng F) \ ( Carrier KL))) by SUBSET_1:def 4

      .= (( rng F) /\ ( Carrier KL)) by XBOOLE_1: 48

      .= ( Carrier KL) by A2, XBOOLE_1: 28;

      for k st k in ( dom (KL (#) G2)) holds ((KL (#) G2) /. k) = ( 0. V1)

      proof

        let k such that

         A6: k in ( dom (KL (#) G2));

        ( len (KL (#) G2)) = ( len G2) by VECTSP_6:def 5;

        then

         A7: ( dom (KL (#) G2)) = ( dom G2) by FINSEQ_3: 29;

        then (G2 . k) in ( rng G2) by A6, FUNCT_1:def 3;

        then (G2 . k) in (( rng F) \ ( Carrier KL)) by FINSEQ_3: 65;

        then not (G2 . k) in ( Carrier KL) by XBOOLE_0:def 5;

        then

         A8: not (G2 /. k) in ( Carrier KL) by A6, A7, PARTFUN1:def 6;

        reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

        

        thus ((KL (#) G2) /. k) = ((KL (#) G2) . k) by A6, PARTFUN1:def 6

        .= ((KL . (G2 /. k1)) * (G2 /. k1)) by A6, VECTSP_6:def 5

        .= (( 0. K) * (G2 /. k)) by A8, VECTSP_6: 2

        .= ( 0. V1) by VECTSP_1: 14;

      end;

      then

       A9: ( Sum (KL (#) G2)) = ( 0. V1) by Th11;

      (KL (#) (G1 ^ G2)) = ((KL (#) F) * p1) by A3, Th19;

      

      hence ( Sum (KL (#) F)) = ( Sum (KL (#) (G1 ^ G2))) by RLVECT_2: 7

      .= ( Sum ((KL (#) G1) ^ (KL (#) G2))) by VECTSP_6: 13

      .= (( Sum (KL (#) G1)) + ( Sum (KL (#) G2))) by RLVECT_1: 41

      .= (( Sum KL) + ( 0. V1)) by A4, A5, A9, VECTSP_6:def 6

      .= ( Sum KL) by RLVECT_1: 4;

    end;

    theorem :: MATRLIN:21

    

     Th21: for A be set holds for p be FinSequence of V1 st ( rng p) c= A holds f1 is additive homogeneous & f2 is additive homogeneous & (for v st v in A holds (f1 . v) = (f2 . v)) implies (f1 . ( Sum p)) = (f2 . ( Sum p))

    proof

      let A be set;

      let p be FinSequence of V1 such that

       A1: ( rng p) c= A;

      defpred P[ FinSequence of V1] means ( rng $1) c= A implies (f1 . ( Sum $1)) = (f2 . ( Sum $1));

      assume

       A2: f1 is additive homogeneous;

      assume

       A3: f2 is additive homogeneous;

      assume

       A4: for v st v in A holds (f1 . v) = (f2 . v);

      

       A5: for p be FinSequence of V1, x be Element of V1 st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence of V1, x be Element of V1 such that

         A6: ( rng p) c= A implies (f1 . ( Sum p)) = (f2 . ( Sum p));

        

         A7: ( rng p) c= (( rng p) \/ ( rng <*x*>)) by XBOOLE_1: 7;

        assume ( rng (p ^ <*x*>)) c= A;

        then

         A8: (( rng p) \/ ( rng <*x*>)) c= A by FINSEQ_1: 31;

        ( rng <*x*>) c= (( rng p) \/ ( rng <*x*>)) by XBOOLE_1: 7;

        then ( rng <*x*>) c= A by A8;

        then {x} c= A by FINSEQ_1: 39;

        then

         A9: x in A by ZFMISC_1: 31;

        

        thus (f1 . ( Sum (p ^ <*x*>))) = (f1 . (( Sum p) + ( Sum <*x*>))) by RLVECT_1: 41

        .= ((f2 . ( Sum p)) + (f1 . ( Sum <*x*>))) by A2, A6, A8, A7, VECTSP_1:def 20

        .= ((f2 . ( Sum p)) + (f1 . x)) by RLVECT_1: 44

        .= ((f2 . ( Sum p)) + (f2 . x)) by A4, A9

        .= ((f2 . ( Sum p)) + (f2 . ( Sum <*x*>))) by RLVECT_1: 44

        .= (f2 . (( Sum p) + ( Sum <*x*>))) by A3, VECTSP_1:def 20

        .= (f2 . ( Sum (p ^ <*x*>))) by RLVECT_1: 41;

      end;

      

       A10: P[( <*> the carrier of V1)]

      proof

        assume ( rng ( <*> the carrier of V1)) c= A;

        

        thus (f1 . ( Sum ( <*> the carrier of V1))) = (f1 . ( 0. V1)) by RLVECT_1: 43

        .= (f1 . (( 0. K) * ( 0. V1))) by VECTSP_1: 14

        .= (( 0. K) * (f1 . ( 0. V1))) by A2, MOD_2:def 2

        .= ( 0. V2) by VECTSP_1: 14

        .= (( 0. K) * (f2 . ( 0. V1))) by VECTSP_1: 14

        .= (f2 . (( 0. K) * ( 0. V1))) by A3, MOD_2:def 2

        .= (f2 . ( 0. V1)) by VECTSP_1: 14

        .= (f2 . ( Sum ( <*> the carrier of V1))) by RLVECT_1: 43;

      end;

      for p be FinSequence of V1 holds P[p] from FINSEQ_2:sch 2( A10, A5);

      hence thesis by A1;

    end;

    theorem :: MATRLIN:22

    

     Th22: f1 is additive homogeneous & f2 is additive homogeneous implies for b1 be OrdBasis of V1 st ( len b1) > 0 holds (f1 * b1) = (f2 * b1) implies f1 = f2

    proof

      assume that

       A1: f1 is additive homogeneous and

       A2: f2 is additive homogeneous;

      let b1 be OrdBasis of V1 such that

       A3: ( len b1) > 0 ;

      reconsider b = ( rng b1) as Basis of V1 by Def2;

      assume

       A4: (f1 * b1) = (f2 * b1);

      now

        ( len b1) in ( Seg ( len b1)) by A3, FINSEQ_1: 3;

        then

        reconsider D = ( dom b1) as non empty set by FINSEQ_1:def 3;

        let v be Element of V1;

        ( Lin b) = the ModuleStr of V1 by VECTSP_7:def 3;

        then v in ( Lin b) by RLVECT_1: 1;

        then

        consider KL be Linear_Combination of b such that

         A5: v = ( Sum KL) by VECTSP_7: 7;

        set p = (KL (#) b1);

        set A = the set of all ((KL . (b1 /. i)) * (b1 /. i)) where i be Element of D;

        

         A6: ( rng p) c= A

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider i be Nat such that

           A7: i in ( dom p) and

           A8: (p . i) = x by FINSEQ_2: 10;

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

          then i in ( Seg ( len b1)) by A7, VECTSP_6:def 5;

          then

           A9: i in ( dom b1) by FINSEQ_1:def 3;

          ((KL (#) b1) . i) = ((KL . (b1 /. i)) * (b1 /. i)) by A7, VECTSP_6:def 5;

          hence thesis by A8, A9;

        end;

        

         A10: for w st w in A holds (f1 . w) = (f2 . w)

        proof

          let w;

          assume w in A;

          then

          consider i be Element of D such that

           A11: w = ((KL . (b1 /. i)) * (b1 /. i));

          (f1 . (b1 /. i)) = (f1 . (b1 . i)) by PARTFUN1:def 6

          .= ((f2 * b1) . i) by A4, FUNCT_1: 13

          .= (f2 . (b1 . i)) by FUNCT_1: 13

          .= (f2 . (b1 /. i)) by PARTFUN1:def 6;

          

          then (f1 . ((KL . (b1 /. i)) * (b1 /. i))) = ((KL . (b1 /. i)) * (f2 . (b1 /. i))) by A1, MOD_2:def 2

          .= (f2 . ((KL . (b1 /. i)) * (b1 /. i))) by A2, MOD_2:def 2;

          hence thesis by A11;

        end;

        

         A12: b1 is one-to-one & ( Carrier KL) c= ( rng b1) by Def2, VECTSP_6:def 4;

        

        hence (f1 . v) = (f1 . ( Sum (KL (#) b1))) by A5, Th20

        .= (f2 . ( Sum p)) by A1, A2, A6, A10, Th21

        .= (f2 . v) by A5, A12, Th20;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    registration

      let D be non empty set;

      cluster -> FinSequence-yielding for Matrix of D;

      coherence ;

    end

    definition

      let D be non empty set;

      let F,G be Matrix of D;

      :: original: ^^

      redefine

      func F ^^ G -> Matrix of D ;

      coherence

      proof

        reconsider M = (F ^^ G) as FinSequence;

        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 n = (( width F) + ( width G));

          let x;

          

           A1: ( rng F) c= (D * ) & ( rng G) c= (D * ) by FINSEQ_1:def 4;

          assume x in ( rng M);

          then

          consider y be object such that

           A2: y in ( dom M) and

           A3: x = (M . y) by FUNCT_1:def 3;

          

           A4: ( dom M) = (( dom F) /\ ( dom G)) by PRE_POLY:def 4;

          then

           A5: y in ( dom G) by A2, XBOOLE_0:def 4;

          then

           A6: (G . y) in ( rng G) by FUNCT_1:def 3;

          

           A7: y in ( dom F) by A2, A4, XBOOLE_0:def 4;

          then (F . y) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider f = (F . y), g = (G . y) as FinSequence of D by A6, A1, FINSEQ_1:def 11;

          reconsider y as Nat by A2, FINSEQ_3: 23;

          

           A8: (G . y) = ( Line (G,y)) by A5, MATRIX_0: 60;

          

           A9: x = (f ^ g) by A2, A3, PRE_POLY:def 4;

          then

          reconsider p = x as FinSequence of D;

          take p;

          thus x = p;

          (F . y) = ( Line (F,y)) by A7, MATRIX_0: 60;

          

          hence ( len p) = (( len ( Line (F,y))) + ( len ( Line (G,y)))) by A9, A8, FINSEQ_1: 22

          .= (( width F) + ( len ( Line (G,y)))) by MATRIX_0:def 7

          .= n by MATRIX_0:def 7;

        end;

        hence thesis by MATRIX_0: 9;

      end;

    end

    definition

      let D be non empty set;

      let n, m, k;

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

      :: original: ^

      redefine

      func M1 ^ M2 -> Matrix of (n + m), k, D ;

      coherence

      proof

        per cases ;

          suppose

           A1: n = 0 ;

          then ( len M1) = 0 by MATRIX_0:def 2;

          then M1 = {} ;

          hence thesis by A1, FINSEQ_1: 34;

        end;

          suppose

           A2: m = 0 ;

          then ( len M2) = 0 by MATRIX_0:def 2;

          then M2 = {} ;

          hence thesis by A2, FINSEQ_1: 34;

        end;

          suppose that

           A3: n <> 0 and

           A4: m <> 0 ;

          ( len M2) = m by MATRIX_0:def 2;

          then

           A5: ( width M2) = k by A4, MATRIX_0: 20;

          ( len M1) = n by MATRIX_0:def 2;

          then

           A6: ( width M1) = k by A3, MATRIX_0: 20;

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

          proof

            take k;

            let x such that

             A7: x in ( rng (M1 ^ M2));

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

            then

            reconsider p = x as FinSequence of D by A7, FINSEQ_1:def 11;

            take p;

            

             A8: x in (( rng M1) \/ ( rng M2)) by A7, FINSEQ_1: 31;

            now

              per cases by A8, XBOOLE_0:def 3;

                suppose x in ( rng M1);

                then

                consider y1 be object such that

                 A9: y1 in ( dom M1) and

                 A10: x = (M1 . y1) by FUNCT_1:def 3;

                reconsider y1 as Nat by A9, FINSEQ_3: 23;

                x = ( Line (M1,y1)) by A9, A10, MATRIX_0: 60;

                hence ( len p) = k by A6, MATRIX_0:def 7;

              end;

                suppose x in ( rng M2);

                then

                consider y2 be object such that

                 A11: y2 in ( dom M2) and

                 A12: x = (M2 . y2) by FUNCT_1:def 3;

                reconsider y2 as Nat by A11, FINSEQ_3: 23;

                x = ( Line (M2,y2)) by A11, A12, MATRIX_0: 60;

                hence ( len p) = k by A5, MATRIX_0:def 7;

              end;

            end;

            hence thesis;

          end;

          then

          reconsider M3 = (M1 ^ M2) as Matrix of D by MATRIX_0: 9;

          ( len M1) = n & ( len M2) = m by MATRIX_0:def 2;

          then

           A13: ( len M3) = (n + m) by FINSEQ_1: 22;

          then

          consider s be FinSequence such that

           A14: s in ( rng M3) and

           A15: ( len s) = ( width M3) by A3, MATRIX_0:def 3;

          

           A16: s in (( rng M1) \/ ( rng M2)) by A14, FINSEQ_1: 31;

          now

            per cases by A16, XBOOLE_0:def 3;

              suppose s in ( rng M1);

              then

              consider y1 be object such that

               A17: y1 in ( dom M1) and

               A18: s = (M1 . y1) by FUNCT_1:def 3;

              reconsider y1 as Nat by A17, FINSEQ_3: 23;

              s = ( Line (M1,y1)) by A17, A18, MATRIX_0: 60;

              hence ( width M3) = k by A6, A15, MATRIX_0:def 7;

            end;

              suppose s in ( rng M2);

              then

              consider y2 be object such that

               A19: y2 in ( dom M2) and

               A20: s = (M2 . y2) by FUNCT_1:def 3;

              reconsider y2 as Nat by A19, FINSEQ_3: 23;

              s = ( Line (M2,y2)) by A19, A20, MATRIX_0: 60;

              hence ( width M3) = k by A5, A15, MATRIX_0:def 7;

            end;

          end;

          hence thesis by A3, A13, MATRIX_0: 20;

        end;

      end;

    end

    theorem :: MATRLIN:23

    for M1 be Matrix of n, k, D, M2 be Matrix of m, k, D st i in ( dom M1) holds ( Line ((M1 ^ M2),i)) = ( Line (M1,i))

    proof

      let M1 be Matrix of n, k, D;

      let M2 be Matrix of m, k, D such that

       A1: i in ( dom M1);

      reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

      ( dom M1) c= ( dom (M1 ^ M2)) by FINSEQ_1: 26;

      

      hence ( Line ((M1 ^ M2),i)) = ((M1 ^ M2) . i) by A1, MATRIX_0: 60

      .= (M1 . i1) by A1, FINSEQ_1:def 7

      .= ( Line (M1,i)) by A1, MATRIX_0: 60;

    end;

    theorem :: MATRLIN:24

    

     Th24: for M1 be Matrix of n, k, D, M2 be Matrix of m, k, D st ( width M1) = ( width M2) holds ( width (M1 ^ M2)) = ( width M1)

    proof

      let M1 be Matrix of n, k, D;

      let M2 be Matrix of m, k, D such that

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

      consider n such that

       A2: for x st x in ( rng (M1 ^ M2)) holds ex P be FinSequence of D st x = P & ( len P) = n by MATRIX_0: 9;

      per cases ;

        suppose

         A3: ( len (M1 ^ M2)) = 0 ;

        then (( len M1) + ( len M2)) = 0 by FINSEQ_1: 22;

        then

         A4: ( len M1) = 0 ;

        ( width (M1 ^ M2)) = 0 by A3, MATRIX_0:def 3

        .= ( width M1) by A4, MATRIX_0:def 3;

        hence thesis;

      end;

        suppose

         A5: ( len (M1 ^ M2)) > 0 ;

        then

         A6: (( len M1) + ( len M2)) > ( 0 + 0 ) by FINSEQ_1: 22;

        consider s be FinSequence such that

         A7: s in ( rng (M1 ^ M2)) and

         A8: ( len s) = ( width (M1 ^ M2)) by A5, MATRIX_0:def 3;

        

         A9: ex P be FinSequence of D st s = P & ( len P) = n by A2, A7;

        per cases by A6;

          suppose ( len M1) > 0 ;

          then

          consider s1 be FinSequence such that

           A10: s1 in ( rng M1) and

           A11: ( len s1) = ( width M1) by MATRIX_0:def 3;

          ( rng M1) c= ( rng (M1 ^ M2)) by FINSEQ_1: 29;

          then ex P1 be FinSequence of D st s1 = P1 & ( len P1) = n by A2, A10;

          hence thesis by A8, A9, A11;

        end;

          suppose ( len M2) > 0 ;

          then

          consider s2 be FinSequence such that

           A12: s2 in ( rng M2) and

           A13: ( len s2) = ( width M2) by MATRIX_0:def 3;

          ( rng M2) c= ( rng (M1 ^ M2)) by FINSEQ_1: 30;

          then ex P2 be FinSequence of D st s2 = P2 & ( len P2) = n by A2, A12;

          hence thesis by A1, A8, A9, A13;

        end;

      end;

    end;

    theorem :: MATRLIN:25

    for M1 be Matrix of t, k, D, M2 be Matrix of m, k, D st n in ( dom M2) & i = (( len M1) + n) holds ( Line ((M1 ^ M2),i)) = ( Line (M2,n))

    proof

      let M1 be Matrix of t, k, D;

      let M2 be Matrix of m, k, D;

      assume that

       A1: n in ( dom M2) and

       A2: i = (( len M1) + n);

      reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

      i in ( dom (M1 ^ M2)) by A1, A2, FINSEQ_1: 28;

      

      hence ( Line ((M1 ^ M2),i)) = ((M1 ^ M2) . i) by MATRIX_0: 60

      .= (M2 . n1) by A1, A2, FINSEQ_1:def 7

      .= ( Line (M2,n)) by A1, MATRIX_0: 60;

    end;

    theorem :: MATRLIN:26

    

     Th26: for M1 be Matrix of n, k, D, M2 be Matrix of m, k, D st ( width M1) = ( width M2) holds for i st i in ( Seg ( width M1)) holds ( Col ((M1 ^ M2),i)) = (( Col (M1,i)) ^ ( Col (M2,i)))

    proof

      let M1 be Matrix of n, k, D;

      let M2 be Matrix of m, k, D such that

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

      let i such that

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

      

       A3: ( dom ( Col ((M1 ^ M2),i))) = ( Seg ( len ( Col ((M1 ^ M2),i)))) by FINSEQ_1:def 3;

      

       A4: ( len ( Col ((M1 ^ M2),i))) = ( len (M1 ^ M2)) by MATRIX_0:def 8

      .= (( len M1) + ( len M2)) by FINSEQ_1: 22

      .= (( len M1) + ( len ( Col (M2,i)))) by MATRIX_0:def 8

      .= (( len ( Col (M1,i))) + ( len ( Col (M2,i)))) by MATRIX_0:def 8

      .= ( len (( Col (M1,i)) ^ ( Col (M2,i)))) by FINSEQ_1: 22;

      now

        let j be Nat;

        assume

         A5: j in ( dom ( Col ((M1 ^ M2),i)));

        then j in ( Seg ( len (M1 ^ M2))) by A3, MATRIX_0:def 8;

        then

         A6: j in ( dom (M1 ^ M2)) by FINSEQ_1:def 3;

        i in ( Seg ( width (M1 ^ M2))) by A1, A2, Th24;

        then [j, i] in [:( dom (M1 ^ M2)), ( Seg ( width (M1 ^ M2))):] by A6, ZFMISC_1: 87;

        then [j, i] in ( Indices (M1 ^ M2)) by MATRIX_0:def 4;

        then

        consider P be FinSequence of D such that

         A7: P = ((M1 ^ M2) . j) and

         A8: ((M1 ^ M2) * (j,i)) = (P . i) by MATRIX_0:def 5;

        

         A9: j in ( dom (( Col (M1,i)) ^ ( Col (M2,i)))) by A4, A3, A5, FINSEQ_1:def 3;

        now

          per cases by A9, FINSEQ_1: 25;

            suppose

             A10: j in ( dom ( Col (M1,i)));

            then j in ( Seg ( len ( Col (M1,i)))) by FINSEQ_1:def 3;

            then j in ( Seg ( len M1)) by MATRIX_0:def 8;

            then

             A11: j in ( dom M1) by FINSEQ_1:def 3;

            then [j, i] in [:( dom M1), ( Seg ( width M1)):] by A2, ZFMISC_1: 87;

            then [j, i] in ( Indices M1) by MATRIX_0:def 4;

            then

            consider P1 be FinSequence of D such that

             A12: P1 = (M1 . j) and

             A13: (M1 * (j,i)) = (P1 . i) by MATRIX_0:def 5;

            P = P1 by A7, A11, A12, FINSEQ_1:def 7;

            

            hence (( Col ((M1 ^ M2),i)) . j) = (M1 * (j,i)) by A6, A8, A13, MATRIX_0:def 8

            .= (( Col (M1,i)) . j) by A11, MATRIX_0:def 8

            .= ((( Col (M1,i)) ^ ( Col (M2,i))) . j) by A10, FINSEQ_1:def 7;

          end;

            suppose ex n be Nat st n in ( dom ( Col (M2,i))) & j = (( len ( Col (M1,i))) + n);

            then

            consider n be Nat such that

             A14: n in ( dom ( Col (M2,i))) and

             A15: j = (( len ( Col (M1,i))) + n);

            n in ( Seg ( len ( Col (M2,i)))) by A14, FINSEQ_1:def 3;

            then n in ( Seg ( len M2)) by MATRIX_0:def 8;

            then

             A16: n in ( dom M2) by FINSEQ_1:def 3;

            then [n, i] in [:( dom M2), ( Seg ( width M2)):] by A1, A2, ZFMISC_1: 87;

            then [n, i] in ( Indices M2) by MATRIX_0:def 4;

            then

            consider P2 be FinSequence of D such that

             A17: P2 = (M2 . n) and

             A18: (M2 * (n,i)) = (P2 . i) by MATRIX_0:def 5;

            ( len ( Col (M2,i))) = ( len M2) by MATRIX_0:def 8;

            then ( len ( Col (M1,i))) = ( len M1) & ( dom ( Col (M2,i))) = ( dom M2) by FINSEQ_3: 29, MATRIX_0:def 8;

            then P = P2 by A7, A14, A15, A17, FINSEQ_1:def 7;

            

            hence (( Col ((M1 ^ M2),i)) . j) = (M2 * (n,i)) by A6, A8, A18, MATRIX_0:def 8

            .= (( Col (M2,i)) . n) by A16, MATRIX_0:def 8

            .= ((( Col (M1,i)) ^ ( Col (M2,i))) . j) by A14, A15, FINSEQ_1:def 7;

          end;

        end;

        hence (( Col ((M1 ^ M2),i)) . j) = ((( Col (M1,i)) ^ ( Col (M2,i))) . j);

      end;

      hence thesis by A4, FINSEQ_2: 9;

    end;

    theorem :: MATRLIN:27

    

     Th27: for M1 be Matrix of n, k, the carrier of V, M2 be Matrix of m, k, the carrier of V holds ( Sum (M1 ^ M2)) = (( Sum M1) ^ ( Sum M2))

    proof

      let M1 be Matrix of n, k, the carrier of V;

      let M2 be Matrix of m, k, the carrier of V;

      

       A1: ( dom ( Sum (M1 ^ M2))) = ( Seg ( len ( Sum (M1 ^ M2)))) by FINSEQ_1:def 3;

       A2:

      now

        let i be Nat;

        assume

         A3: i in ( dom ( Sum (M1 ^ M2)));

        then i in ( Seg ( len (M1 ^ M2))) by A1, Def6;

        then

         A4: i in ( dom (M1 ^ M2)) by FINSEQ_1:def 3;

        now

          per cases by A4, FINSEQ_1: 25;

            suppose

             A5: i in ( dom M1);

            ( len M1) = ( len ( Sum M1)) by Def6;

            then

             A6: ( dom M1) = ( dom ( Sum M1)) by FINSEQ_3: 29;

            

            thus (( Sum (M1 ^ M2)) . i) = (( Sum (M1 ^ M2)) /. i) by A3, PARTFUN1:def 6

            .= ( Sum ((M1 ^ M2) /. i)) by A3, Def6

            .= ( Sum (M1 /. i)) by A5, FINSEQ_4: 68

            .= (( Sum M1) /. i) by A5, A6, Def6

            .= (( Sum M1) . i) by A5, A6, PARTFUN1:def 6

            .= ((( Sum M1) ^ ( Sum M2)) . i) by A5, A6, FINSEQ_1:def 7;

          end;

            suppose

             A7: ex n be Nat st n in ( dom M2) & i = (( len M1) + n);

            

             A8: ( len M1) = ( len ( Sum M1)) by Def6;

            ( len M2) = ( len ( Sum M2)) by Def6;

            then

             A9: ( dom M2) = ( dom ( Sum M2)) by FINSEQ_3: 29;

            consider n be Nat such that

             A10: n in ( dom M2) and

             A11: i = (( len M1) + n) by A7;

            

            thus (( Sum (M1 ^ M2)) . i) = (( Sum (M1 ^ M2)) /. i) by A3, PARTFUN1:def 6

            .= ( Sum ((M1 ^ M2) /. i)) by A3, Def6

            .= ( Sum (M2 /. n)) by A10, A11, FINSEQ_4: 69

            .= (( Sum M2) /. n) by A10, A9, Def6

            .= (( Sum M2) . n) by A10, A9, PARTFUN1:def 6

            .= ((( Sum M1) ^ ( Sum M2)) . i) by A10, A11, A8, A9, FINSEQ_1:def 7;

          end;

        end;

        hence (( Sum (M1 ^ M2)) . i) = ((( Sum M1) ^ ( Sum M2)) . i);

      end;

      ( len ( Sum (M1 ^ M2))) = ( len (M1 ^ M2)) by Def6

      .= (( len M1) + ( len M2)) by FINSEQ_1: 22

      .= (( len ( Sum M1)) + ( len M2)) by Def6

      .= (( len ( Sum M1)) + ( len ( Sum M2))) by Def6

      .= ( len (( Sum M1) ^ ( Sum M2))) by FINSEQ_1: 22;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: MATRLIN:28

    

     Th28: for M1 be Matrix of n, k, D, M2 be Matrix of m, k, D st ( width M1) = ( width M2) holds ((M1 ^ M2) @ ) = ((M1 @ ) ^^ (M2 @ ))

    proof

      let M1 be Matrix of n, k, D;

      let M2 be Matrix of m, k, D such that

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

      

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

      .= (( dom (M1 @ )) /\ ( dom (M2 @ ))) by PRE_POLY:def 4

      .= (( dom (M1 @ )) /\ ( Seg ( len (M2 @ )))) by FINSEQ_1:def 3

      .= (( Seg ( len (M1 @ ))) /\ ( Seg ( len (M2 @ )))) by FINSEQ_1:def 3

      .= (( Seg ( width M1)) /\ ( Seg ( len (M2 @ )))) by MATRIX_0:def 6

      .= (( Seg ( width M1)) /\ ( Seg ( width M2))) by MATRIX_0:def 6

      .= ( Seg ( width M1)) by A1;

      

       A3: ( dom ((M1 ^ M2) @ )) = ( Seg ( len ((M1 ^ M2) @ ))) by FINSEQ_1:def 3;

      

       A4: ( len ((M1 ^ M2) @ )) = ( width (M1 ^ M2)) by MATRIX_0:def 6

      .= ( width M1) by A1, Th24

      .= ( len ((M1 @ ) ^^ (M2 @ ))) by A2, FINSEQ_1: 6;

      now

        let i be Nat;

        assume

         A5: i in ( dom ((M1 ^ M2) @ ));

        then

         A6: i in ( Seg ( width (M1 ^ M2))) by A3, MATRIX_0:def 6;

        

         A7: i in ( dom ((M1 @ ) ^^ (M2 @ ))) by A4, A3, A5, FINSEQ_1:def 3;

        then

         A8: i in (( dom (M1 @ )) /\ ( dom (M2 @ ))) by PRE_POLY:def 4;

        then

         A9: i in ( dom (M2 @ )) by XBOOLE_0:def 4;

        

         A10: i in ( dom (M1 @ )) by A8, XBOOLE_0:def 4;

        reconsider m1 = ((M1 @ ) . i), m2 = ((M2 @ ) . i) as FinSequence;

        i in (( Seg ( len (M1 @ ))) /\ ( dom (M2 @ ))) by A8, FINSEQ_1:def 3;

        then i in (( Seg ( len (M1 @ ))) /\ ( Seg ( len (M2 @ )))) by FINSEQ_1:def 3;

        then i in (( Seg ( width M1)) /\ ( Seg ( len (M2 @ )))) by MATRIX_0:def 6;

        then

         A11: i in (( Seg ( width M1)) /\ ( Seg ( width M2))) by MATRIX_0:def 6;

        

        thus (((M1 ^ M2) @ ) . i) = ( Line (((M1 ^ M2) @ ),i)) by A5, MATRIX_0: 60

        .= ( Col ((M1 ^ M2),i)) by A6, MATRIX_0: 59

        .= (( Col (M1,i)) ^ ( Col (M2,i))) by A1, A11, Th26

        .= (( Line ((M1 @ ),i)) ^ ( Col (M2,i))) by A1, A11, MATRIX_0: 59

        .= (( Line ((M1 @ ),i)) ^ ( Line ((M2 @ ),i))) by A1, A11, MATRIX_0: 59

        .= (( Line ((M1 @ ),i)) ^ m2) by A9, MATRIX_0: 60

        .= (m1 ^ m2) by A10, MATRIX_0: 60

        .= (((M1 @ ) ^^ (M2 @ )) . i) by A7, PRE_POLY:def 4;

      end;

      hence thesis by A4, FINSEQ_2: 9;

    end;

    theorem :: MATRLIN:29

    

     Th29: for M1,M2 be Matrix of the carrier of V1 holds (( Sum M1) + ( Sum M2)) = ( Sum (M1 ^^ M2))

    proof

      let M1,M2 be Matrix of the carrier of V1;

      reconsider m = ( min (( len M1),( len M2))) as Element of NAT by ORDINAL1:def 12;

      

       A1: ( Seg m) = (( Seg ( len M1)) /\ ( Seg ( len M2))) by FINSEQ_2: 2

      .= (( Seg ( len M1)) /\ ( dom M2)) by FINSEQ_1:def 3

      .= (( dom M1) /\ ( dom M2)) by FINSEQ_1:def 3

      .= ( dom (M1 ^^ M2)) by PRE_POLY:def 4

      .= ( Seg ( len (M1 ^^ M2))) by FINSEQ_1:def 3;

      

       A2: ( len (( Sum M1) + ( Sum M2))) = ( min (( len ( Sum M1)),( len ( Sum M2)))) by FINSEQ_2: 71

      .= ( min (( len M1),( len ( Sum M2)))) by Def6

      .= ( min (( len M1),( len M2))) by Def6

      .= ( len (M1 ^^ M2)) by A1, FINSEQ_1: 6

      .= ( len ( Sum (M1 ^^ M2))) by Def6;

      

       A3: ( dom (( Sum M1) + ( Sum M2))) = ( Seg ( len (( Sum M1) + ( Sum M2)))) by FINSEQ_1:def 3;

      now

        let i be Nat;

        assume

         A4: i in ( dom (( Sum M1) + ( Sum M2)));

        then

         A5: i in ( dom ( Sum (M1 ^^ M2))) by A2, A3, FINSEQ_1:def 3;

        i in ( Seg ( len (M1 ^^ M2))) by A2, A3, A4, Def6;

        then

         A6: i in ( dom (M1 ^^ M2)) by FINSEQ_1:def 3;

        then

         A7: i in (( dom M1) /\ ( dom M2)) by PRE_POLY:def 4;

        then

         A8: i in ( dom M1) by XBOOLE_0:def 4;

        

         A9: i in ( dom M2) by A7, XBOOLE_0:def 4;

        reconsider m1 = (M1 . i), m2 = (M2 . i) as FinSequence;

        

         A10: ((M1 /. i) ^ (M2 /. i)) = (m1 ^ (M2 /. i)) by A8, PARTFUN1:def 6

        .= (m1 ^ m2) by A9, PARTFUN1:def 6

        .= ((M1 ^^ M2) . i) by A6, PRE_POLY:def 4

        .= ((M1 ^^ M2) /. i) by A6, PARTFUN1:def 6;

        i in ( Seg ( len M2)) by A9, FINSEQ_1:def 3;

        then i in ( Seg ( len ( Sum M2))) by Def6;

        then

         A11: i in ( dom ( Sum M2)) by FINSEQ_1:def 3;

        then

         A12: (( Sum M2) /. i) = (( Sum M2) . i) by PARTFUN1:def 6;

        i in ( Seg ( len M1)) by A8, FINSEQ_1:def 3;

        then i in ( Seg ( len ( Sum M1))) by Def6;

        then

         A13: i in ( dom ( Sum M1)) by FINSEQ_1:def 3;

        then (( Sum M1) /. i) = (( Sum M1) . i) by PARTFUN1:def 6;

        

        hence ((( Sum M1) + ( Sum M2)) . i) = ((( Sum M1) /. i) + (( Sum M2) /. i)) by A4, A12, FUNCOP_1: 22

        .= (( Sum (M1 /. i)) + (( Sum M2) /. i)) by A13, Def6

        .= (( Sum (M1 /. i)) + ( Sum (M2 /. i))) by A11, Def6

        .= ( Sum ((M1 ^^ M2) /. i)) by A10, RLVECT_1: 41

        .= (( Sum (M1 ^^ M2)) /. i) by A5, Def6

        .= (( Sum (M1 ^^ M2)) . i) by A5, PARTFUN1:def 6;

      end;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: MATRLIN:30

    

     Th30: for P1,P2 be FinSequence of V1 st ( len P1) = ( len P2) holds ( Sum (P1 + P2)) = (( Sum P1) + ( Sum P2))

    proof

      let P1,P2 be FinSequence of V1;

      assume ( len P1) = ( len P2);

      then

      reconsider R1 = P1, R2 = P2 as Element of (( len P1) -tuples_on the carrier of V1) by FINSEQ_2: 92;

      

      thus ( Sum (P1 + P2)) = ( Sum (R1 + R2))

      .= (( Sum P1) + ( Sum P2)) by FVSUM_1: 76;

    end;

    theorem :: MATRLIN:31

    

     Th31: for M1,M2 be Matrix of the carrier of V1 st ( len M1) = ( len M2) holds (( Sum ( Sum M1)) + ( Sum ( Sum M2))) = ( Sum ( Sum (M1 ^^ M2)))

    proof

      let M1,M2 be Matrix of the carrier of V1 such that

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

      ( len ( Sum M1)) = ( len M1) by Def6

      .= ( len ( Sum M2)) by A1, Def6;

      

      hence (( Sum ( Sum M1)) + ( Sum ( Sum M2))) = ( Sum (( Sum M1) + ( Sum M2))) by Th30

      .= ( Sum ( Sum (M1 ^^ M2))) by Th29;

    end;

    theorem :: MATRLIN:32

    

     Th32: for M be Matrix of the carrier of V1 holds ( Sum ( Sum M)) = ( Sum ( Sum (M @ )))

    proof

      defpred X[ Nat] means for M be Matrix of the carrier of V1 st ( len M) = $1 holds ( Sum ( Sum M)) = ( Sum ( Sum (M @ )));

      let M be Matrix of the carrier of V1;

      

       A1: for P be FinSequence of V1 holds ( Sum ( Sum <*P*>)) = ( Sum ( Sum ( <*P*> @ )))

      proof

        defpred X[ FinSequence of V1] means ( Sum ( Sum <*$1*>)) = ( Sum ( Sum ( <*$1*> @ )));

        let P be FinSequence of V1;

        ( len <*( <*> the carrier of V1)*>) = 1 by MATRIX_0:def 2;

        then ( width <*( <*> the carrier of V1)*>) = 0 by MATRIX_0: 20;

        then

         A2: ( len ( <*( <*> the carrier of V1)*> @ )) = 0 by MATRIX_0:def 6;

        

         A3: for P be FinSequence of V1, x be Element of V1 st X[P] holds X[(P ^ <*x*>)]

        proof

          let P be FinSequence of V1, x be Element of V1 such that

           A4: ( Sum ( Sum <*P*>)) = ( Sum ( Sum ( <*P*> @ )));

          ( Seg ( len ( <*P*> ^^ <* <*x*>*>))) = ( dom ( <*P*> ^^ <* <*x*>*>)) by FINSEQ_1:def 3

          .= (( dom <*P*>) /\ ( dom <* <*x*>*>)) by PRE_POLY:def 4

          .= (( Seg 1) /\ ( dom <* <*x*>*>)) by FINSEQ_1: 38

          .= (( Seg 1) /\ ( Seg 1)) by FINSEQ_1: 38

          .= ( Seg 1);

          

          then

           A5: ( len ( <*P*> ^^ <* <*x*>*>)) = 1 by FINSEQ_1: 6

          .= ( len <*(P ^ <*x*>)*>) by FINSEQ_1: 39;

          then

           A6: ( dom ( <*P*> ^^ <* <*x*>*>)) = ( Seg ( len <*(P ^ <*x*>)*>)) by FINSEQ_1:def 3;

           A7:

          now

            let i be Nat;

            assume

             A8: i in ( dom ( <*P*> ^^ <* <*x*>*>));

            then i in {1} by A6, FINSEQ_1: 2, FINSEQ_1: 40;

            then

             A9: i = 1 by TARSKI:def 1;

            reconsider m1 = ( <*P*> . i), m2 = ( <* <*x*>*> . i) as FinSequence;

            

            thus (( <*P*> ^^ <* <*x*>*>) . i) = (m1 ^ m2) by A8, PRE_POLY:def 4

            .= (P ^ m2) by A9, FINSEQ_1: 40

            .= (P ^ <*x*>) by A9, FINSEQ_1: 40

            .= ( <*(P ^ <*x*>)*> . i) by A9, FINSEQ_1: 40;

          end;

          per cases ;

            suppose ( len P) = 0 ;

            then

             A10: P = {} ;

            

            hence ( Sum ( Sum <*(P ^ <*x*>)*>)) = ( Sum ( Sum <* <*x*>*>)) by FINSEQ_1: 34

            .= ( Sum ( Sum ( <* <*x*>*> @ ))) by Th15

            .= ( Sum ( Sum ( <*(P ^ <*x*>)*> @ ))) by A10, FINSEQ_1: 34;

          end;

            suppose

             A11: ( len P) <> 0 ;

            

             A12: ( len <* <*x*>*>) = 1 by FINSEQ_1: 40;

            

            then

             A13: ( width <* <*x*>*>) = ( len <*x*>) by MATRIX_0: 20

            .= 1 by FINSEQ_1: 40;

            then

             A14: ( len ( <* <*x*>*> @ )) = 1 by MATRIX_0:def 6;

            

             A15: ( len <*P*>) = 1 by FINSEQ_1: 40;

            then

             A16: ( width <*P*>) = ( len P) by MATRIX_0: 20;

            then

             A17: ( len ( <*P*> @ )) = ( len P) by MATRIX_0:def 6;

            ( width ( <*P*> @ )) = 1 by A11, A15, A16, MATRIX_0: 54;

            then

            reconsider d1 = ( <*P*> @ ) as Matrix of ( len P), 1, the carrier of V1 by A11, A17, MATRIX_0: 20;

            

             A18: ( len <*(P ^ <*x*>)*>) = 1 by FINSEQ_1: 40;

            

            then

             A19: ( width <*(P ^ <*x*>)*>) = ( len (P ^ <*x*>)) by MATRIX_0: 20

            .= (( len P) + ( len <*x*>)) by FINSEQ_1: 22

            .= (( len P) + 1) by FINSEQ_1: 40;

            

             A20: (( <* <*x*>*> @ ) @ ) = <* <*x*>*> by A12, A13, MATRIX_0: 57;

            

             A21: ( width ( <*P*> @ )) = ( len <*P*>) by A11, A16, MATRIX_0: 54

            .= ( width ( <* <*x*>*> @ )) by A15, A12, A13, MATRIX_0: 54;

            then ( width ( <* <*x*>*> @ )) = 1 by A11, A15, A16, MATRIX_0: 54;

            then

            reconsider d2 = ( <* <*x*>*> @ ) as Matrix of 1, 1, the carrier of V1 by A14, MATRIX_0: 20;

            

             A22: ((d1 ^ d2) @ ) = ((( <*P*> @ ) @ ) ^^ (( <* <*x*>*> @ ) @ )) by A21, Th28

            .= ( <*P*> ^^ <* <*x*>*>) by A11, A15, A16, A20, MATRIX_0: 57

            .= <*(P ^ <*x*>)*> by A5, A7, FINSEQ_2: 9

            .= (( <*(P ^ <*x*>)*> @ ) @ ) by A18, A19, MATRIX_0: 57;

            

             A23: ( len (( <*P*> @ ) ^ ( <* <*x*>*> @ ))) = (( len ( <*P*> @ )) + ( len ( <* <*x*>*> @ ))) by FINSEQ_1: 22

            .= (( width <*P*>) + ( len ( <* <*x*>*> @ ))) by MATRIX_0:def 6

            .= (( width <*P*>) + ( width <* <*x*>*>)) by MATRIX_0:def 6

            .= ( len ( <*(P ^ <*x*>)*> @ )) by A16, A13, A19, MATRIX_0:def 6;

            

            thus ( Sum ( Sum <*(P ^ <*x*>)*>)) = ( Sum ( Sum ( <*P*> ^^ <* <*x*>*>))) by A5, A7, FINSEQ_2: 9

            .= (( Sum ( Sum ( <*P*> @ ))) + ( Sum ( Sum <* <*x*>*>))) by A4, A15, A12, Th31

            .= (( Sum ( Sum ( <*P*> @ ))) + ( Sum ( Sum ( <* <*x*>*> @ )))) by Th15

            .= ( Sum (( Sum d1) ^ ( Sum d2))) by RLVECT_1: 41

            .= ( Sum ( Sum (d1 ^ d2))) by Th27

            .= ( Sum ( Sum ( <*(P ^ <*x*>)*> @ ))) by A23, A22, MATRIX_0: 53;

          end;

        end;

         <*( <*> the carrier of V1)*> is Matrix of ( 0 + 1), 0 , the carrier of V1;

        

        then ( Sum ( Sum <*( <*> the carrier of V1)*>)) = ( 0. V1) by Th14

        .= ( Sum ( Sum ( <*( <*> the carrier of V1)*> @ ))) by A2, Th13;

        then

         A24: X[( <*> the carrier of V1)];

        for P be FinSequence of V1 holds X[P] from FINSEQ_2:sch 2( A24, A3);

        hence thesis;

      end;

      

       A25: for n st X[n] holds X[(n + 1)]

      proof

        let n such that

         A26: for M be Matrix of the carrier of V1 st ( len M) = n holds ( Sum ( Sum M)) = ( Sum ( Sum (M @ )));

        thus for M be Matrix of the carrier of V1 st ( len M) = (n + 1) holds ( Sum ( Sum M)) = ( Sum ( Sum (M @ )))

        proof

          let M be Matrix of the carrier of V1 such that

           A27: ( len M) = (n + 1);

          

           A28: M <> {} by A27;

          

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

          per cases ;

            suppose

             A30: n = 0 ;

            then (M . 1) = ( Line (M,1)) by A27, A29, FINSEQ_1: 4, MATRIX_0: 60;

            then

            reconsider G = (M . 1) as FinSequence of V1;

            M = <*G*> by A27, A30, FINSEQ_1: 40;

            hence thesis by A1;

          end;

            suppose

             A31: n > 0 ;

            

             A32: (M . (n + 1)) = ( Line (M,(n + 1))) by A27, A29, FINSEQ_1: 4, MATRIX_0: 60;

            then

            reconsider M1 = (M . (n + 1)) as FinSequence of V1;

            ( len M1) = ( width M) by A32, MATRIX_0:def 7;

            then

            reconsider R = <*M1*> as Matrix of 1, ( width M), the carrier of V1;

            reconsider M9 = M as Matrix of (n + 1), ( width M), the carrier of V1 by A27, MATRIX_0: 20;

            reconsider W = ( Del (M9,(n + 1))) as Matrix of n, ( width M), the carrier of V1 by Th3;

            

             A33: ( width W) = ( width M9) by A31, Th2

            .= ( width R) by Th2;

            

             A34: ( len (W @ )) = ( width W) by MATRIX_0:def 6

            .= ( len (R @ )) by A33, MATRIX_0:def 6;

            

             A35: ( len ( Del (M,(n + 1)))) = n by A27, Th1;

            

            thus ( Sum ( Sum M)) = ( Sum ( Sum (W ^ R))) by A28, Th4, A27

            .= ( Sum (( Sum W) ^ ( Sum R))) by Th27

            .= (( Sum ( Sum ( Del (M,(n + 1))))) + ( Sum ( Sum R))) by RLVECT_1: 41

            .= (( Sum ( Sum (( Del (M,(n + 1))) @ ))) + ( Sum ( Sum R))) by A26, A35

            .= (( Sum ( Sum (( Del (M,(n + 1))) @ ))) + ( Sum ( Sum (R @ )))) by A1

            .= ( Sum ( Sum ((W @ ) ^^ (R @ )))) by A34, Th31

            .= ( Sum ( Sum ((W ^ R) @ ))) by A33, Th28

            .= ( Sum ( Sum (M @ ))) by A28, Th4, A27;

          end;

        end;

      end;

      

       A36: X[ 0 ]

      proof

        let M be Matrix of the carrier of V1;

        assume

         A37: ( len M) = 0 ;

        then ( width M) = 0 by MATRIX_0:def 3;

        then

         A38: ( len (M @ )) = 0 by MATRIX_0:def 6;

        

        thus ( Sum ( Sum M)) = ( 0. V1) by A37, Th13

        .= ( Sum ( Sum (M @ ))) by A38, Th13;

      end;

      for n holds X[n] from NAT_1:sch 2( A36, A25);

      then X[( len M)];

      hence thesis;

    end;

    theorem :: MATRLIN:33

    

     Th33: for M be Matrix of n, m, the carrier of K st n > 0 & m > 0 holds for p,d be FinSequence of K st ( len p) = n & ( len d) = m & for j st j in ( dom d) holds (d /. j) = ( Sum ( mlt (p,( Col (M,j))))) holds for b,c be FinSequence of V1 st ( len b) = m & ( len c) = n & for i st i in ( dom c) holds (c /. i) = ( Sum ( lmlt (( Line (M,i)),b))) holds ( Sum ( lmlt (p,c))) = ( Sum ( lmlt (d,b)))

    proof

      let M be Matrix of n, m, the carrier of K such that

       A1: n > 0 and

       A2: m > 0 ;

      

       A3: ( len M) = n by A1, MATRIX_0: 23;

      reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;

      let p,d be FinSequence of K such that

       A4: ( len p) = n and

       A5: ( len d) = m and

       A6: for j st j in ( dom d) holds (d /. j) = ( Sum ( mlt (p,( Col (M,j)))));

      let b,c be FinSequence of V1 such that

       A7: ( len b) = m and

       A8: ( len c) = n and

       A9: for i st i in ( dom c) holds (c /. i) = ( Sum ( lmlt (( Line (M,i)),b)));

      deffunc V( Nat, Nat) = (((p /. $1) * (M * ($1,$2))) * (b /. $2));

      consider M1 be Matrix of n1, m1, the carrier of V1 such that

       A10: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = V(i,j) from MATRIX_0:sch 1;

      

       A11: ( width M1) = ( len (M1 @ )) by MATRIX_0:def 6

      .= ( len ( Sum (M1 @ ))) by Def6;

      

       A12: ( dom d) = ( dom b) by A5, A7, FINSEQ_3: 29;

      then

       A13: ( dom ( lmlt (d,b))) = ( dom b) by Th12;

      

      then

       A14: ( len ( lmlt (d,b))) = ( len b) by FINSEQ_3: 29

      .= ( len ( Sum (M1 @ ))) by A1, A7, A11, MATRIX_0: 23;

      then

       A15: ( dom ( lmlt (d,b))) = ( Seg ( len ( Sum (M1 @ )))) by FINSEQ_1:def 3;

      

       A16: ( width M1) = m by A1, MATRIX_0: 23;

      

       A17: ( len M1) = n by A1, MATRIX_0: 23;

      

       A18: ( dom ( lmlt (d,b))) = ( dom d) by A12, Th12;

       A19:

      now

        

         A20: ( Seg ( len ( Sum (M1 @ )))) = ( dom ( Sum (M1 @ ))) by FINSEQ_1:def 3;

        let j be Nat such that

         A21: j in ( dom ( lmlt (d,b)));

        

         A22: j in ( dom ( Sum (M1 @ ))) by A15, A21, FINSEQ_1:def 3;

        

         A23: j in ( dom d) by A12, A21, Th12;

        

         A24: (d /. j) = (d . j) & (b /. j) = (b . j) by A18, A13, A21, PARTFUN1:def 6;

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

        then

         A25: ( dom ( Sum (M1 @ ))) = ( dom (M1 @ )) by FINSEQ_3: 29;

        

        then

         A26: ((M1 @ ) /. j) = ((M1 @ ) . j) by A22, PARTFUN1:def 6

        .= ( Line ((M1 @ ),j)) by A22, A25, MATRIX_0: 60;

        reconsider H = ( mlt (p,( Col (M,j)))) as FinSequence of K;

        deffunc V( Nat) = ((H /. $1) * (b /. j));

        consider G be FinSequence of V1 such that

         A27: ( len G) = ( len p) & for i be Nat st i in ( dom G) holds (G . i) = V(i) from FINSEQ_2:sch 1;

        

         A28: ( len p) = ( len ( Col (M,j))) by A4, A3, MATRIX_0:def 8;

        then

         A29: ( len (the multF of K .: (p,( Col (M,j))))) = ( len p) by FINSEQ_2: 72;

        then

         A30: ( dom H) = ( dom G) by A27, FINSEQ_3: 29;

        

         A31: ( dom p) = ( dom G) by A27, FINSEQ_3: 29;

        

         A32: ( len ( Line ((M1 @ ),j))) = ( width (M1 @ )) by MATRIX_0:def 7

        .= ( len ((M1 @ ) @ )) by MATRIX_0:def 6

        .= ( len G) by A1, A2, A4, A17, A16, A27, MATRIX_0: 57;

        then

         A33: ( dom ( Line ((M1 @ ),j))) = ( Seg ( len G)) by FINSEQ_1:def 3;

        

         A34: ( dom G) = ( Seg ( len p)) by A27, FINSEQ_1:def 3;

         A35:

        now

          let i be Nat;

          

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

          assume

           A37: i in ( dom ( Line ((M1 @ ),j)));

          then

           A38: i in ( Seg ( len (the multF of K .: (p,( Col (M,j)))))) by A27, A28, A33, FINSEQ_2: 72;

          then

           A39: i in ( dom H) by FINSEQ_1:def 3;

          

           A40: i in ( dom (the multF of K .: (p,( Col (M,j))))) by A38, FINSEQ_1:def 3;

          

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

          

          then

           A42: ((p /. i) * (M * (i,j))) = (the multF of K . ((p . i),(M * (i,j)))) by A31, A33, A37, PARTFUN1:def 6

          .= (the multF of K . ((p . i),(( Col (M,j)) . i))) by A4, A3, A27, A33, A37, A36, MATRIX_0:def 8

          .= ((the multF of K .: (p,( Col (M,j)))) . i) by A40, FUNCOP_1: 22

          .= (H /. i) by A39, PARTFUN1:def 6;

          ( dom M1) = ( dom G) by A4, A17, A27, FINSEQ_3: 29;

          then [i, j] in [:( dom M1), ( Seg ( width M1)):] by A11, A15, A21, A33, A37, A41, ZFMISC_1: 87;

          then

           A43: [i, j] in ( Indices M1) by MATRIX_0:def 4;

          i in ( Seg ( width (M1 @ ))) by A32, A33, A37, MATRIX_0:def 7;

          

          hence (( Line ((M1 @ ),j)) . i) = ((M1 @ ) * (j,i)) by MATRIX_0:def 7

          .= (M1 * (i,j)) by A43, MATRIX_0:def 6

          .= ((H /. i) * (b /. j)) by A10, A43, A42

          .= (G . i) by A27, A34, A33, A37;

        end;

        

        thus (( lmlt (d,b)) . j) = (the lmult of V1 . ((d . j),(b . j))) by A21, FUNCOP_1: 22

        .= ((d /. j) * (b /. j)) by A24, VECTSP_1:def 12

        .= (( Sum H) * (b /. j)) by A6, A23

        .= ( Sum G) by A27, A29, A30, Th10

        .= ( Sum ((M1 @ ) /. j)) by A32, A35, A26, FINSEQ_2: 9

        .= (( Sum (M1 @ )) /. j) by A22, Def6

        .= (( Sum (M1 @ )) . j) by A15, A21, A20, PARTFUN1:def 6;

      end;

      

       A44: ( dom p) = ( dom c) by A4, A8, FINSEQ_3: 29;

      then

       A45: ( dom ( lmlt (p,c))) = ( dom p) by Th12;

      

      then

       A46: ( len ( lmlt (p,c))) = ( len p) by FINSEQ_3: 29

      .= ( len M1) by A4, MATRIX_0:def 2

      .= ( len ( Sum M1)) by Def6;

      now

        let i be Nat such that

         A47: i in ( dom ( Sum M1));

        

         A48: i in ( dom c) by A44, A45, A46, A47, FINSEQ_3: 29;

        then

         A49: (c . i) = (c /. i) & (p . i) = (p /. i) by A44, PARTFUN1:def 6;

        i in ( Seg ( len ( Sum M1))) by A47, FINSEQ_1:def 3;

        then i in ( Seg ( len M1)) by Def6;

        then

         A50: i in ( dom M1) by FINSEQ_1:def 3;

        

        then

         A51: (M1 /. i) = (M1 . i) by PARTFUN1:def 6

        .= ( Line (M1,i)) by A50, MATRIX_0: 60;

        deffunc V( Nat) = ((p /. i) * (( lmlt (( Line (M,i)),b)) /. $1));

        consider F be FinSequence of V1 such that

         A52: ( len F) = ( len b) & for j be Nat st j in ( dom F) holds (F . j) = V(j) from FINSEQ_2:sch 1;

        

         A53: ( len F) = ( width M) by A1, A7, A52, MATRIX_0: 23;

        

         A54: ( dom ( Line (M,i))) = ( Seg ( len ( Line (M,i)))) by FINSEQ_1:def 3

        .= ( Seg ( len F)) by A53, MATRIX_0:def 7

        .= ( dom b) by A52, FINSEQ_1:def 3;

        then ( dom ( lmlt (( Line (M,i)),b))) = ( dom b) by Th12;

        then

         A55: ( len F) = ( len ( lmlt (( Line (M,i)),b))) & ( dom F) = ( dom ( lmlt (( Line (M,i)),b))) by A52, FINSEQ_3: 29;

        

         A56: ( len F) = ( width M1) by A1, A7, A52, MATRIX_0: 23;

        then

         A57: ( len ( Line (M1,i))) = ( len F) by MATRIX_0:def 7;

        then

         A58: ( dom (M1 /. i)) = ( Seg ( len F)) by A51, FINSEQ_1:def 3;

        

         A59: ( dom F) = ( Seg ( len b)) by A52, FINSEQ_1:def 3;

         A60:

        now

          let j be Nat;

          assume

           A61: j in ( dom (M1 /. i));

          then

           A62: (( Line (M,i)) . j) = (M * (i,j)) by A53, A58, MATRIX_0:def 7;

           [i, j] in [:( dom M1), ( Seg ( width M1)):] by A56, A50, A58, A61, ZFMISC_1: 87;

          then

           A63: [i, j] in ( Indices M1) by MATRIX_0:def 4;

          

           A64: j in ( dom b) by A52, A58, A61, FINSEQ_1:def 3;

          then

           A65: (b . j) = (b /. j) by PARTFUN1:def 6;

          

           A66: j in ( dom ( lmlt (( Line (M,i)),b))) by A54, A64, Th12;

          

          then

           A67: (( lmlt (( Line (M,i)),b)) /. j) = (( lmlt (( Line (M,i)),b)) . j) by PARTFUN1:def 6

          .= (the lmult of V1 . ((( Line (M,i)) . j),(b . j))) by A66, FUNCOP_1: 22

          .= ((M * (i,j)) * (b /. j)) by A65, A62, VECTSP_1:def 12;

          

          thus ((M1 /. i) . j) = (M1 * (i,j)) by A56, A51, A58, A61, MATRIX_0:def 7

          .= (((p /. i) * (M * (i,j))) * (b /. j)) by A10, A63

          .= ((p /. i) * (( lmlt (( Line (M,i)),b)) /. j)) by A67, VECTSP_1:def 16

          .= (F . j) by A52, A59, A58, A61;

        end;

        

         A68: for j be Nat st j in ( dom F) holds (F . j) = ((p /. i) * (( lmlt (( Line (M,i)),b)) /. j)) by A52;

        i in ( dom (the lmult of V1 .: (p,c))) by A46, A47, FINSEQ_3: 29;

        

        hence (( lmlt (p,c)) . i) = (the lmult of V1 . ((p . i),(c . i))) by FUNCOP_1: 22

        .= ((p /. i) * (c /. i)) by A49, VECTSP_1:def 12

        .= ((p /. i) * ( Sum ( lmlt (( Line (M,i)),b)))) by A9, A48

        .= ( Sum F) by A55, A68, RLVECT_2: 67

        .= ( Sum (M1 /. i)) by A57, A51, A60, FINSEQ_2: 9

        .= (( Sum M1) /. i) by A47, Def6

        .= (( Sum M1) . i) by A47, PARTFUN1:def 6;

      end;

      

      hence ( Sum ( lmlt (p,c))) = ( Sum ( Sum M1)) by A46, FINSEQ_2: 9

      .= ( Sum ( Sum (M1 @ ))) by Th32

      .= ( Sum ( lmlt (d,b))) by A14, A19, FINSEQ_2: 9;

    end;

    begin

    definition

      let K be Field;

      let V be finite-dimensional VectSp of K;

      let b1 be OrdBasis of V;

      let W be Element of V;

      :: MATRLIN:def7

      func W |-- b1 -> FinSequence of K means

      : Def7: ( len it ) = ( len b1) & ex KL be Linear_Combination of V st W = ( Sum KL) & ( Carrier KL) c= ( rng b1) & for k st 1 <= k & k <= ( len it ) holds (it /. k) = (KL . (b1 /. k));

      existence

      proof

        reconsider b2 = ( rng b1) as Basis of V by Def2;

        consider KL be Linear_Combination of V such that

         A1: W = ( Sum KL) and

         A2: ( Carrier KL) c= b2 by Th8;

        deffunc V( Nat) = (KL . (b1 /. $1));

        consider A be FinSequence of K such that

         A3: ( len A) = ( len b1) and

         A4: for k be Nat st k in ( dom A) holds (A . k) = V(k) from FINSEQ_2:sch 1;

        take A;

        thus ( len A) = ( len b1) by A3;

        take KL;

        thus W = ( Sum KL) by A1;

        thus ( Carrier KL) c= ( rng b1) by A2;

        let k;

        

         A5: ( dom A) = ( Seg ( len b1)) by A3, FINSEQ_1:def 3;

        assume 1 <= k & k <= ( len A);

        then

         A6: k in ( Seg ( len b1)) by A3, FINSEQ_1: 1;

        then k in ( dom A) by A3, FINSEQ_1:def 3;

        then (A . k) = (A /. k) by PARTFUN1:def 6;

        hence thesis by A4, A5, A6;

      end;

      uniqueness

      proof

        reconsider b = ( rng b1) as Basis of V by Def2;

        let F1,F2 be FinSequence of K;

        assume

         A7: ( len F1) = ( len b1);

        given KL1 be Linear_Combination of V such that

         A8: W = ( Sum KL1) & ( Carrier KL1) c= ( rng b1) and

         A9: for k st 1 <= k & k <= ( len F1) holds (F1 /. k) = (KL1 . (b1 /. k));

        assume

         A10: ( len F2) = ( len b1);

        given KL2 be Linear_Combination of V such that

         A11: W = ( Sum KL2) & ( Carrier KL2) c= ( rng b1) and

         A12: for k st 1 <= k & k <= ( len F2) holds (F2 /. k) = (KL2 . (b1 /. k));

        

         A13: b is linearly-independent by VECTSP_7:def 3;

        for k be Nat st 1 <= k & k <= ( len F1) holds (F1 . k) = (F2 . k)

        proof

          let k be Nat;

          assume

           A14: 1 <= k & k <= ( len F1);

          then

           A15: k in ( dom F2) by A7, A10, FINSEQ_3: 25;

          k in ( dom F1) by A14, FINSEQ_3: 25;

          

          hence (F1 . k) = (F1 /. k) by PARTFUN1:def 6

          .= (KL1 . (b1 /. k)) by A9, A14

          .= (KL2 . (b1 /. k)) by A8, A11, A13, Th5

          .= (F2 /. k) by A7, A10, A12, A14

          .= (F2 . k) by A15, PARTFUN1:def 6;

        end;

        hence thesis by A7, A10, FINSEQ_1: 14;

      end;

    end

    

     Lm1: for K be Field holds for V be finite-dimensional VectSp of K holds for b be OrdBasis of V holds for W be Element of V holds ( dom (W |-- b)) = ( dom b)

    proof

      let K be Field, V be finite-dimensional VectSp of K, b be OrdBasis of V, W be Element of V;

      ( len (W |-- b)) = ( len b) by Def7;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: MATRLIN:34

    

     Th34: (v1 |-- b2) = (v2 |-- b2) implies v1 = v2

    proof

      consider KL1 be Linear_Combination of V2 such that

       A1: v1 = ( Sum KL1) and

       A2: ( Carrier KL1) c= ( rng b2) and

       A3: for t st 1 <= t & t <= ( len (v1 |-- b2)) holds ((v1 |-- b2) /. t) = (KL1 . (b2 /. t)) by Def7;

      consider KL2 be Linear_Combination of V2 such that

       A4: v2 = ( Sum KL2) and

       A5: ( Carrier KL2) c= ( rng b2) and

       A6: for t st 1 <= t & t <= ( len (v2 |-- b2)) holds ((v2 |-- b2) /. t) = (KL2 . (b2 /. t)) by Def7;

      assume

       A7: (v1 |-- b2) = (v2 |-- b2);

       A8:

      now

        let t be Nat;

        assume

         A9: 1 <= t & t <= ( len (v1 |-- b2));

        

        hence (KL1 . (b2 /. t)) = ((v2 |-- b2) /. t) by A7, A3

        .= (KL2 . (b2 /. t)) by A7, A6, A9;

      end;

      

       A10: (( Carrier KL1) \/ ( Carrier KL2)) c= ( rng b2) by A2, A5, XBOOLE_1: 8;

      now

        let v be Vector of V2;

        per cases ;

          suppose

           A11: not v in (( Carrier KL1) \/ ( Carrier KL2));

          then not v in ( Carrier KL2) by XBOOLE_0:def 3;

          then

           A12: (KL2 . v) = ( 0. K) by VECTSP_6: 2;

           not v in ( Carrier KL1) by A11, XBOOLE_0:def 3;

          hence (KL1 . v) = (KL2 . v) by A12, VECTSP_6: 2;

        end;

          suppose v in (( Carrier KL1) \/ ( Carrier KL2));

          then

          consider x be object such that

           A13: x in ( dom b2) and

           A14: v = (b2 . x) by A10, FUNCT_1:def 3;

          reconsider x as Nat by A13, FINSEQ_3: 23;

          x <= ( len b2) by A13, FINSEQ_3: 25;

          then

           A15: x <= ( len (v1 |-- b2)) by Def7;

          v = (b2 /. x) & 1 <= x by A13, A14, FINSEQ_3: 25, PARTFUN1:def 6;

          hence (KL1 . v) = (KL2 . v) by A8, A15;

        end;

      end;

      hence thesis by A1, A4, VECTSP_6:def 7;

    end;

    theorem :: MATRLIN:35

    

     Th35: v = ( Sum ( lmlt ((v |-- b1),b1)))

    proof

      consider KL be Linear_Combination of V1 such that

       A1: v = ( Sum KL) & ( Carrier KL) c= ( rng b1) and

       A2: for k st 1 <= k & k <= ( len (v |-- b1)) holds ((v |-- b1) /. k) = (KL . (b1 /. k)) by Def7;

      ( len (v |-- b1)) = ( len b1) by Def7;

      then

       A3: ( dom (v |-- b1)) = ( dom b1) by FINSEQ_3: 29;

      then

       A4: ( dom b1) = ( dom ( lmlt ((v |-- b1),b1))) by Th12;

      ( len (KL (#) b1)) = ( len b1) by VECTSP_6:def 5

      .= ( len ( lmlt ((v |-- b1),b1))) by A4, FINSEQ_3: 29;

      then

       A5: ( dom (KL (#) b1)) = ( dom ( lmlt ((v |-- b1),b1))) by FINSEQ_3: 29;

       A6:

      now

        let t be Nat;

        assume

         A7: t in ( dom ( lmlt ((v |-- b1),b1)));

        then

         A8: (b1 /. t) = (b1 . t) by A4, PARTFUN1:def 6;

        t in ( dom (v |-- b1)) by A3, A7, Th12;

        then

         A9: t <= ( len (v |-- b1)) by FINSEQ_3: 25;

        

         A10: 1 <= t by A7, FINSEQ_3: 25;

        then

         A11: ((v |-- b1) /. t) = ((v |-- b1) . t) by A9, FINSEQ_4: 15;

        t in ( dom (KL (#) b1)) by A5, A7;

        

        hence ((KL (#) b1) . t) = ((KL . (b1 /. t)) * (b1 /. t)) by VECTSP_6:def 5

        .= (((v |-- b1) /. t) * (b1 /. t)) by A2, A10, A9

        .= (the lmult of V1 . (((v |-- b1) . t),(b1 . t))) by A8, A11, VECTSP_1:def 12

        .= (( lmlt ((v |-- b1),b1)) . t) by A7, FUNCOP_1: 22;

      end;

      b1 is one-to-one by Def2;

      

      hence v = ( Sum (KL (#) b1)) by A1, Th20

      .= ( Sum ( lmlt ((v |-- b1),b1))) by A5, A6, FINSEQ_1: 13;

    end;

    theorem :: MATRLIN:36

    

     Th36: ( len d) = ( len b1) implies d = (( Sum ( lmlt (d,b1))) |-- b1)

    proof

      reconsider T = ( rng b1) as finite Subset of V1 by Def2;

      defpred X[ Element of V1, Element of K] means ($1 in ( rng b1) implies (for k st k in ( dom b1) & (b1 /. k) = $1 holds $2 = (d /. k))) & ( not $1 in ( rng b1) implies $2 = ( 0. K));

      

       A1: for v holds ex u be Element of K st X[v, u]

      proof

        let v be Element of V1;

        per cases ;

          suppose

           A2: v in ( rng b1);

          then

          consider k be Element of NAT such that

           A3: k in ( dom b1) and

           A4: (b1 /. k) = v by PARTFUN2: 2;

          take u = (d /. k);

          now

            

             A5: b1 is one-to-one by Def2;

            let i;

            assume that

             A6: i in ( dom b1) and

             A7: (b1 /. i) = v;

            (b1 . i) = (b1 /. k) by A4, A6, A7, PARTFUN1:def 6

            .= (b1 . k) by A3, PARTFUN1:def 6;

            hence u = (d /. i) by A3, A6, A5, FUNCT_1:def 4;

          end;

          hence thesis by A2;

        end;

          suppose

           A8: not v in ( rng b1);

          take ( 0. K);

          thus thesis by A8;

        end;

      end;

      consider KL be Function of V1, K such that

       A9: for v holds X[v, (KL . v)] from FUNCT_2:sch 3( A1);

       A10:

      now

        take T;

        let v be Element of V1;

        assume not v in T;

        hence (KL . v) = ( 0. K) by A9;

      end;

      now

        take f = KL;

        thus KL = f & ( dom f) = the carrier of V1 & ( rng f) c= the carrier of K by FUNCT_2:def 1, RELAT_1:def 19;

      end;

      then KL in ( Funcs (the carrier of V1,the carrier of K)) by FUNCT_2:def 2;

      then

      reconsider KL1 = KL as Linear_Combination of V1 by A10, VECTSP_6:def 1;

      assume

       A11: ( len d) = ( len b1);

      now

        take KL1;

        

         A12: b1 is one-to-one by Def2;

        thus

         A13: for k st 1 <= k & k <= ( len d) holds (d /. k) = (KL1 . (b1 /. k))

        proof

          let k;

          assume 1 <= k & k <= ( len d);

          then

           A14: k in ( dom b1) by A11, FINSEQ_3: 25;

          then (b1 . k) = (b1 /. k) by PARTFUN1:def 6;

          then (b1 /. k) in ( rng b1) by A14, FUNCT_1:def 3;

          hence thesis by A9, A14;

        end;

        for x be object holds x in ( Carrier KL1) implies x in ( rng b1)

        proof

          let x be object;

          assume x in ( Carrier KL1);

          then

           A15: ex v st x = v & (KL1 . v) <> ( 0. K) by VECTSP_6: 1;

          assume not x in ( rng b1);

          hence contradiction by A9, A15;

        end;

        hence

         A16: ( Carrier KL1) c= ( rng b1);

        

         A17: ( dom d) = ( dom b1) by A11, FINSEQ_3: 29;

        then

         A18: ( dom ( lmlt (d,b1))) = ( dom b1) by Th12;

        

        then

         A19: ( len ( lmlt (d,b1))) = ( len b1) by FINSEQ_3: 29

        .= ( len (KL1 (#) b1)) by VECTSP_6:def 5;

        now

          let k be Nat;

          assume

           A20: k in ( dom ( lmlt (d,b1)));

          then

           A21: k in ( dom (KL1 (#) b1)) by A19, FINSEQ_3: 29;

          

           A22: 1 <= k & k <= ( len d) by A11, A18, A20, FINSEQ_3: 25;

          

           A23: (d /. k) = (d . k) & (b1 /. k) = (b1 . k) by A17, A18, A20, PARTFUN1:def 6;

          

          thus (( lmlt (d,b1)) . k) = (the lmult of V1 . ((d . k),(b1 . k))) by A20, FUNCOP_1: 22

          .= ((d /. k) * (b1 /. k)) by A23, VECTSP_1:def 12

          .= ((KL1 . (b1 /. k)) * (b1 /. k)) by A13, A22

          .= ((KL1 (#) b1) . k) by A21, VECTSP_6:def 5;

        end;

        

        hence ( Sum ( lmlt (d,b1))) = ( Sum (KL1 (#) b1)) by A19, FINSEQ_2: 9

        .= ( Sum KL1) by A16, A12, Th20;

      end;

      hence thesis by A11, Def7;

    end;

    

     Lm2: for p be FinSequence, k be set st k in ( dom p) holds ( len p) > 0

    proof

      let p be FinSequence, k be set;

      assume k in ( dom p);

      then p <> {} ;

      hence thesis;

    end;

    theorem :: MATRLIN:37

    

     Th37: for a,d be FinSequence of K st ( len a) = ( len b1) holds for j be Nat st j in ( dom b2) & ( len d) = ( len b1) & for k st k in ( dom b1) holds (d . k) = (((f . (b1 /. k)) |-- b2) /. j) holds ( len b1) > 0 implies ((( Sum ( lmlt (a,(f * b1)))) |-- b2) /. j) = ( Sum ( mlt (a,d)))

    proof

      let a,d be FinSequence of K such that

       A1: ( len a) = ( len b1);

      reconsider B3 = (f * b1) as FinSequence of V2;

      deffunc V( Nat, Nat) = (((B3 /. $1) |-- b2) /. $2);

      consider M be Matrix of ( len b1), ( len b2), the carrier of K such that

       A2: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = V(i,j) from MATRIX_0:sch 1;

      deffunc W( Nat) = ( Sum ( mlt (a,( Col (M,$1)))));

      consider dd be FinSequence of K such that

       A3: ( len dd) = ( len b2) & for j be Nat st j in ( dom dd) holds (dd /. j) = W(j) from FINSEQ_4:sch 2;

      let j be Nat such that

       A4: j in ( dom b2);

      

       A5: j in ( dom dd) by A4, A3, FINSEQ_3: 29;

      assume that

       A6: ( len d) = ( len b1) and

       A7: for k st k in ( dom b1) holds (d . k) = (((f . (b1 /. k)) |-- b2) /. j);

      

       A8: ( len ( Col (M,j))) = ( len M) by MATRIX_0:def 8

      .= ( len d) by A6, MATRIX_0:def 2;

      ( len M) = ( len b1) by MATRIX_0:def 2;

      then

       A9: ( dom M) = ( dom b1) by FINSEQ_3: 29;

      

       A10: ( len b1) = ( len B3) by FINSEQ_2: 33;

      then

       A11: ( dom b1) = ( dom B3) by FINSEQ_3: 29;

      assume

       A12: ( len b1) > 0 ;

      then

       A13: ( width M) = ( len b2) by MATRIX_0: 23;

       A14:

      now

        let i such that

         A15: i in ( dom B3);

         A16:

        now

          let j be Nat;

          assume

           A17: j in ( dom ((B3 /. i) |-- b2));

          then j in ( Seg ( len ((B3 /. i) |-- b2))) by FINSEQ_1:def 3;

          then

           A18: j in ( Seg ( width M)) by A13, Def7;

          then [i, j] in [:( dom M), ( Seg ( width M)):] by A9, A11, A15, ZFMISC_1: 87;

          then

           A19: [i, j] in ( Indices M) by MATRIX_0:def 4;

          

          thus (( Line (M,i)) . j) = (M * (i,j)) by A18, MATRIX_0:def 7

          .= (((B3 /. i) |-- b2) /. j) by A2, A19

          .= (((B3 /. i) |-- b2) . j) by A17, PARTFUN1:def 6;

        end;

        

         A20: ( len ( Line (M,i))) = ( width M) by MATRIX_0:def 7

        .= ( len ((B3 /. i) |-- b2)) by A13, Def7;

        

        thus (B3 /. i) = ( Sum ( lmlt (((B3 /. i) |-- b2),b2))) by Th35

        .= ( Sum ( lmlt (( Line (M,i)),b2))) by A20, A16, FINSEQ_2: 9;

      end;

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

      then

       A21: j in ( Seg ( width M)) by A4, A12, MATRIX_0: 23;

       A22:

      now

        let i be Nat;

        assume i in ( dom d);

        then

         A23: i in ( dom b1) by A6, FINSEQ_3: 29;

        

        then

         A24: (B3 /. i) = (B3 . i) by A11, PARTFUN1:def 6

        .= (f . (b1 . i)) by A23, FUNCT_1: 13

        .= (f . (b1 /. i)) by A23, PARTFUN1:def 6;

         [i, j] in [:( dom M), ( Seg ( width M)):] by A9, A21, A23, ZFMISC_1: 87;

        then

         A25: [i, j] in ( Indices M) by MATRIX_0:def 4;

        

        thus (( Col (M,j)) . i) = (M * (i,j)) by A9, A23, MATRIX_0:def 8

        .= (((f . (b1 /. i)) |-- b2) /. j) by A2, A24, A25

        .= (d . i) by A7, A23;

      end;

      ( len b2) > 0 by A4, Lm2;

      

      hence ((( Sum ( lmlt (a,(f * b1)))) |-- b2) /. j) = ((( Sum ( lmlt (dd,b2))) |-- b2) /. j) by A1, A12, A3, A10, A14, Th33

      .= (dd /. j) by A3, Th36

      .= ( Sum ( mlt (a,( Col (M,j))))) by A3, A5

      .= ( Sum ( mlt (a,d))) by A8, A22, FINSEQ_2: 9;

    end;

    begin

    definition

      let K be Field;

      let V1,V2 be finite-dimensional VectSp of K;

      let f be Function of V1, V2;

      let b1 be FinSequence of V1;

      let b2 be OrdBasis of V2;

      :: MATRLIN:def8

      func AutMt (f,b1,b2) -> Matrix of K means

      : Def8: ( len it ) = ( len b1) & for k st k in ( dom b1) holds (it /. k) = ((f . (b1 /. k)) |-- b2);

      existence

      proof

        deffunc V( Nat) = ((f . (b1 /. $1)) |-- b2);

        consider M be FinSequence such that

         A1: ( len M) = ( len b1) and

         A2: for k be Nat st k in ( dom M) holds (M . k) = V(k) from FINSEQ_1:sch 2;

        

         A3: ( dom M) = ( Seg ( len b1)) by A1, FINSEQ_1:def 3;

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

        proof

          take n = ( len ((f . (b1 /. 1)) |-- b2));

          let x be object;

          assume x in ( rng M);

          then

          consider y be object such that

           A4: y in ( dom M) and

           A5: x = (M . y) by FUNCT_1:def 3;

          reconsider y as Nat by A4, FINSEQ_3: 23;

          (M . y) = ((f . (b1 /. y)) |-- b2) by A2, A4;

          then

          reconsider s = (M . y) as FinSequence;

          take s;

          thus s = x by A5;

          

          thus ( len s) = ( len ((f . (b1 /. y)) |-- b2)) by A2, A4

          .= ( len b2) by Def7

          .= n by Def7;

        end;

        then

        reconsider M as tabular FinSequence by MATRIX_0:def 1;

        now

          let x be object;

          assume x in ( rng M);

          then

          consider y be object such that

           A6: y in ( dom M) and

           A7: x = (M . y) by FUNCT_1:def 3;

          reconsider y as Nat by A6, FINSEQ_3: 23;

          (M . y) = ((f . (b1 /. y)) |-- b2) by A2, A6;

          then

          reconsider s = (M . y) as FinSequence of K;

          s = x by A7;

          hence x in (the carrier of K * ) by FINSEQ_1:def 11;

        end;

        then ( rng M) c= (the carrier of K * );

        then

        reconsider M as Matrix of K by FINSEQ_1:def 4;

        take M1 = M;

        for k st k in ( dom b1) holds (M1 /. k) = ((f . (b1 /. k)) |-- b2)

        proof

          let k be Nat;

          assume

           A8: k in ( dom b1);

          then

           A9: k in ( Seg ( len b1)) by FINSEQ_1:def 3;

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

          

          hence (M1 /. k) = (M1 . k) by A8, PARTFUN1:def 6

          .= ((f . (b1 /. k)) |-- b2) by A2, A3, A9;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let K1,K2 be Matrix of K such that

         A10: ( len K1) = ( len b1) and

         A11: for k st k in ( dom b1) holds (K1 /. k) = ((f . (b1 /. k)) |-- b2) and

         A12: ( len K2) = ( len b1) and

         A13: for k st k in ( dom b1) holds (K2 /. k) = ((f . (b1 /. k)) |-- b2);

        for k be Nat st 1 <= k & k <= ( len K1) holds (K1 . k) = (K2 . k)

        proof

          let k be Nat;

          assume

           A14: 1 <= k & k <= ( len K1);

          then

           A15: k in ( dom b1) by A10, FINSEQ_3: 25;

          

           A16: k in ( dom K2) by A10, A12, A14, FINSEQ_3: 25;

          k in ( dom K1) by A14, FINSEQ_3: 25;

          

          hence (K1 . k) = (K1 /. k) by PARTFUN1:def 6

          .= ((f . (b1 /. k)) |-- b2) by A11, A15

          .= (K2 /. k) by A13, A15

          .= (K2 . k) by A16, PARTFUN1:def 6;

        end;

        hence thesis by A10, A12, FINSEQ_1: 14;

      end;

    end

    

     Lm3: ( dom ( AutMt (f,b1,b2))) = ( dom b1)

    proof

      ( len ( AutMt (f,b1,b2))) = ( len b1) by Def8;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: MATRLIN:38

    

     Th38: ( len b1) = 0 implies ( AutMt (f,b1,b2)) = {}

    proof

      assume ( len b1) = 0 ;

      then ( len ( AutMt (f,b1,b2))) = 0 by Def8;

      hence thesis;

    end;

    theorem :: MATRLIN:39

    

     Th39: ( len b1) > 0 implies ( width ( AutMt (f,b1,b2))) = ( len b2)

    proof

      assume ( len b1) > 0 ;

      then ( len ( AutMt (f,b1,b2))) > 0 by Def8;

      then

      consider s be FinSequence such that

       A1: s in ( rng ( AutMt (f,b1,b2))) and

       A2: ( len s) = ( width ( AutMt (f,b1,b2))) by MATRIX_0:def 3;

      consider i be Nat such that

       A3: i in ( dom ( AutMt (f,b1,b2))) and

       A4: (( AutMt (f,b1,b2)) . i) = s by A1, FINSEQ_2: 10;

      ( len ( AutMt (f,b1,b2))) = ( len b1) by Def8;

      then

       A5: i in ( dom b1) by A3, FINSEQ_3: 29;

      s = (( AutMt (f,b1,b2)) /. i) by A3, A4, PARTFUN1:def 6

      .= ((f . (b1 /. i)) |-- b2) by A5, Def8;

      hence thesis by A2, Def7;

    end;

    theorem :: MATRLIN:40

    f1 is additive homogeneous & f2 is additive homogeneous & ( AutMt (f1,b1,b2)) = ( AutMt (f2,b1,b2)) & ( len b1) > 0 implies f1 = f2

    proof

      assume that

       A1: f1 is additive homogeneous & f2 is additive homogeneous and

       A2: ( AutMt (f1,b1,b2)) = ( AutMt (f2,b1,b2)) and

       A3: ( len b1) > 0 ;

      ( rng b1) is Basis of V1 by Def2;

      then

       A4: ( rng b1) c= the carrier of V1;

      then

       A5: ( rng b1) c= ( dom f2) by FUNCT_2:def 1;

      ( rng b1) c= ( dom f1) by A4, FUNCT_2:def 1;

      

      then

       A6: ( dom (f1 * b1)) = ( dom b1) by RELAT_1: 27

      .= ( dom (f2 * b1)) by A5, RELAT_1: 27;

      now

        let x be object;

        assume

         A7: x in ( dom (f1 * b1));

        then

        reconsider k = x as Nat by FINSEQ_3: 23;

        

         A8: ( dom (f1 * b1)) c= ( dom b1) by RELAT_1: 25;

        

        then

         A9: ((f1 . (b1 /. k)) |-- b2) = (( AutMt (f2,b1,b2)) /. k) by A2, A7, Def8

        .= ((f2 . (b1 /. k)) |-- b2) by A7, A8, Def8;

        

        thus ((f1 * b1) . x) = (f1 . (b1 . x)) by A7, FUNCT_1: 12

        .= (f1 . (b1 /. x)) by A7, A8, PARTFUN1:def 6

        .= (f2 . (b1 /. x)) by A9, Th34

        .= (f2 . (b1 . x)) by A7, A8, PARTFUN1:def 6

        .= ((f2 * b1) . x) by A6, A7, FUNCT_1: 12;

      end;

      hence thesis by A1, A3, A6, Th22, FUNCT_1: 2;

    end;

    theorem :: MATRLIN:41

    g is additive homogeneous & ( len b1) > 0 & ( len b2) > 0 implies ( AutMt ((g * f),b1,b3)) = (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))

    proof

      assume

       A1: g is additive homogeneous;

      assume that

       A2: ( len b1) > 0 and

       A3: ( len b2) > 0 ;

      

       A4: ( width ( AutMt (f,b1,b2))) = ( len b2) by A2, Th39

      .= ( len ( AutMt (g,b2,b3))) by Def8;

      

       A5: ( width ( AutMt ((g * f),b1,b3))) = ( len b3) by A2, Th39

      .= ( width ( AutMt (g,b2,b3))) by A3, Th39;

      then

       A6: ( width ( AutMt ((g * f),b1,b3))) = ( width (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))) by A4, MATRIX_3:def 4;

      

       A7: ( len ( AutMt ((g * f),b1,b3))) = ( len b1) by Def8

      .= ( len ( AutMt (f,b1,b2))) by Def8

      .= ( len (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))) by A4, MATRIX_3:def 4;

      then

       A8: ( dom ( AutMt ((g * f),b1,b3))) = ( dom (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))) by FINSEQ_3: 29;

      for i, j st [i, j] in ( Indices ( AutMt ((g * f),b1,b3))) holds (( AutMt ((g * f),b1,b3)) * (i,j)) = ((( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3))) * (i,j))

      proof

        let i, j;

        deffunc V( Nat) = (((g . (b2 /. $1)) |-- b3) /. j);

        consider d be FinSequence of K such that

         A9: ( len d) = ( len b2) & for k be Nat st k in ( dom d) holds (d . k) = V(k) from FINSEQ_2:sch 1;

        assume

         A10: [i, j] in ( Indices ( AutMt ((g * f),b1,b3)));

        then

         A11: [i, j] in [:( dom ( AutMt ((g * f),b1,b3))), ( Seg ( width ( AutMt ((g * f),b1,b3)))):] by MATRIX_0:def 4;

        then

         A12: j in ( Seg ( width ( AutMt ((g * f),b1,b3)))) by ZFMISC_1: 87;

        

         A13: ( len ( Col (( AutMt (g,b2,b3)),j))) = ( len ( AutMt (g,b2,b3))) by MATRIX_0:def 8

        .= ( len d) by A9, Def8;

        

         A14: ( dom d) = ( Seg ( len b2)) by A9, FINSEQ_1:def 3;

        

         A15: [i, j] in ( Indices (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))) by A8, A6, A11, MATRIX_0:def 4;

        

         A16: i in ( dom ( AutMt ((g * f),b1,b3))) by A11, ZFMISC_1: 87;

        

         A17: ( width ( AutMt ((g * f),b1,b3))) <> {} by A12;

        ( len b1) = ( len ( AutMt ((g * f),b1,b3))) by Def8;

        then ( len b1) > 0 by A17, MATRIX_0:def 3;

        then

         A18: j in ( Seg ( len b3)) by A12, Th39;

        then

         A19: j in ( dom b3) by FINSEQ_1:def 3;

         A20:

        now

          let k be Nat;

          assume

           A21: 1 <= k & k <= ( len d);

          then

           A22: k in ( dom d) by FINSEQ_3: 25;

          

           A23: k in ( dom b2) by A9, A21, FINSEQ_3: 25;

          

           A24: ( len ( AutMt (g,b2,b3))) = ( len b2) by Def8;

          then

           A25: k in ( dom ( AutMt (g,b2,b3))) by A9, A21, FINSEQ_3: 25;

          j in ( Seg ( width ( AutMt (g,b2,b3)))) by A5, A11, ZFMISC_1: 87;

          then [k, j] in [:( dom ( AutMt (g,b2,b3))), ( Seg ( width ( AutMt (g,b2,b3)))):] by A25, ZFMISC_1: 87;

          then [k, j] in ( Indices ( AutMt (g,b2,b3))) by MATRIX_0:def 4;

          then

          consider p2 be FinSequence of K such that

           A26: p2 = (( AutMt (g,b2,b3)) . k) and

           A27: (( AutMt (g,b2,b3)) * (k,j)) = (p2 . j) by MATRIX_0:def 5;

          

           A28: p2 = (( AutMt (g,b2,b3)) /. k) by A25, A26, PARTFUN1:def 6

          .= ((g . (b2 /. k)) |-- b3) by A23, Def8;

          then j in ( Seg ( len p2)) by A18, Def7;

          then

           A29: j in ( dom p2) by FINSEQ_1:def 3;

          k in ( dom ( AutMt (g,b2,b3))) by A9, A21, A24, FINSEQ_3: 25;

          

          hence (( Col (( AutMt (g,b2,b3)),j)) . k) = (p2 . j) by A27, MATRIX_0:def 8

          .= (((g . (b2 /. k)) |-- b3) /. j) by A28, A29, PARTFUN1:def 6

          .= (d . k) by A9, A22;

        end;

        (b1 /. i) in the carrier of V1;

        then

         A30: (b1 /. i) in ( dom f) by FUNCT_2:def 1;

        consider p1 be FinSequence of K such that

         A31: p1 = (( AutMt ((g * f),b1,b3)) . i) and

         A32: (( AutMt ((g * f),b1,b3)) * (i,j)) = (p1 . j) by A10, MATRIX_0:def 5;

        

         A33: ( len ((f . (b1 /. i)) |-- b2)) = ( len b2) by Def7;

        

         A34: ( len ( AutMt ((g * f),b1,b3))) = ( len b1) by Def8;

        then

         A35: i in ( dom b1) by A16, FINSEQ_3: 29;

        

         A36: p1 = (( AutMt ((g * f),b1,b3)) /. i) by A16, A31, PARTFUN1:def 6

        .= (((g * f) . (b1 /. i)) |-- b3) by A35, Def8;

        ( len ( AutMt (f,b1,b2))) = ( len b1) by Def8;

        then

         A37: i in ( dom ( AutMt (f,b1,b2))) by A16, A34, FINSEQ_3: 29;

        

        then

         A38: ( Line (( AutMt (f,b1,b2)),i)) = (( AutMt (f,b1,b2)) . i) by MATRIX_0: 60

        .= (( AutMt (f,b1,b2)) /. i) by A37, PARTFUN1:def 6

        .= ((f . (b1 /. i)) |-- b2) by A35, Def8;

        

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

        j in ( Seg ( len (((g * f) . (b1 /. i)) |-- b3))) by A18, Def7;

        then j in ( dom p1) by A36, FINSEQ_1:def 3;

        

        hence (( AutMt ((g * f),b1,b3)) * (i,j)) = ((((g * f) . (b1 /. i)) |-- b3) /. j) by A32, A36, PARTFUN1:def 6

        .= (((g . (f . (b1 /. i))) |-- b3) /. j) by A30, FUNCT_1: 13

        .= (((g . ( Sum ( lmlt (((f . (b1 /. i)) |-- b2),b2)))) |-- b3) /. j) by Th35

        .= ((( Sum ( lmlt (((f . (b1 /. i)) |-- b2),(g * b2)))) |-- b3) /. j) by A1, A33, Th18

        .= ( Sum ( mlt (((f . (b1 /. i)) |-- b2),d))) by A3, A19, A9, A14, A39, A33, Th37

        .= (( Line (( AutMt (f,b1,b2)),i)) "*" ( Col (( AutMt (g,b2,b3)),j))) by A38, A13, A20, FINSEQ_1: 14

        .= ((( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3))) * (i,j)) by A4, A15, MATRIX_3:def 4;

      end;

      hence thesis by A7, A6, MATRIX_0: 21;

    end;

    theorem :: MATRLIN:42

    ( AutMt ((f1 + f2),b1,b2)) = (( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2)))

    proof

      

       A1: ( len ( AutMt ((f1 + f2),b1,b2))) = ( len b1) by Def8

      .= ( len ( AutMt (f1,b1,b2))) by Def8;

      then

       A2: ( dom ( AutMt ((f1 + f2),b1,b2))) = ( dom ( AutMt (f1,b1,b2))) by FINSEQ_3: 29;

      

       A3: ( width ( AutMt (f1,b1,b2))) = ( width ( AutMt (f2,b1,b2)))

      proof

        per cases ;

          suppose

           A4: ( len b1) = 0 ;

          

          then ( AutMt (f1,b1,b2)) = {} by Th38

          .= ( AutMt (f2,b1,b2)) by A4, Th38;

          hence thesis;

        end;

          suppose

           A5: ( len b1) > 0 ;

          

          hence ( width ( AutMt (f1,b1,b2))) = ( len b2) by Th39

          .= ( width ( AutMt (f2,b1,b2))) by A5, Th39;

        end;

      end;

      

       A6: ( width ( AutMt ((f1 + f2),b1,b2))) = ( width ( AutMt (f1,b1,b2)))

      proof

        per cases ;

          suppose

           A7: ( len b1) = 0 ;

          

          then ( AutMt ((f1 + f2),b1,b2)) = {} by Th38

          .= ( AutMt (f1,b1,b2)) by A7, Th38;

          hence thesis;

        end;

          suppose

           A8: ( len b1) > 0 ;

          

          hence ( width ( AutMt ((f1 + f2),b1,b2))) = ( len b2) by Th39

          .= ( width ( AutMt (f1,b1,b2))) by A8, Th39;

        end;

      end;

      then

       A9: ( width ( AutMt ((f1 + f2),b1,b2))) = ( width (( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2)))) by MATRIX_3:def 3;

      ( len ( AutMt (f1,b1,b2))) = ( len b1) by Def8

      .= ( len ( AutMt (f2,b1,b2))) by Def8;

      then

       A10: ( dom ( AutMt (f1,b1,b2))) = ( dom ( AutMt (f2,b1,b2))) by FINSEQ_3: 29;

      

       A11: for i, j st [i, j] in ( Indices ( AutMt ((f1 + f2),b1,b2))) holds (( AutMt ((f1 + f2),b1,b2)) * (i,j)) = ((( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2))) * (i,j))

      proof

        let i, j;

        assume

         A12: [i, j] in ( Indices ( AutMt ((f1 + f2),b1,b2)));

        then

         A13: [i, j] in [:( dom ( AutMt ((f1 + f2),b1,b2))), ( Seg ( width ( AutMt ((f1 + f2),b1,b2)))):] by MATRIX_0:def 4;

        then

         A14: [i, j] in ( Indices ( AutMt (f1,b1,b2))) by A2, A6, MATRIX_0:def 4;

        

         A15: [i, j] in ( Indices ( AutMt (f2,b1,b2))) by A10, A3, A2, A6, A13, MATRIX_0:def 4;

        (( AutMt ((f1 + f2),b1,b2)) * (i,j)) = ((( AutMt (f1,b1,b2)) * (i,j)) + (( AutMt (f2,b1,b2)) * (i,j)))

        proof

          consider KL3 be Linear_Combination of V2 such that

           A16: (f2 . (b1 /. i)) = ( Sum KL3) & ( Carrier KL3) c= ( rng b2) and

           A17: for t st 1 <= t & t <= ( len ((f2 . (b1 /. i)) |-- b2)) holds (((f2 . (b1 /. i)) |-- b2) /. t) = (KL3 . (b2 /. t)) by Def7;

          consider KL2 be Linear_Combination of V2 such that

           A18: (f1 . (b1 /. i)) = ( Sum KL2) & ( Carrier KL2) c= ( rng b2) and

           A19: for t st 1 <= t & t <= ( len ((f1 . (b1 /. i)) |-- b2)) holds (((f1 . (b1 /. i)) |-- b2) /. t) = (KL2 . (b2 /. t)) by Def7;

          

           A20: i in ( dom ( AutMt ((f1 + f2),b1,b2))) by A13, ZFMISC_1: 87;

          then

           A21: i in ( dom b1) by Lm3;

          reconsider b4 = ( rng b2) as Basis of V2 by Def2;

          consider p1 be FinSequence of K such that

           A22: p1 = (( AutMt ((f1 + f2),b1,b2)) . i) and

           A23: (( AutMt ((f1 + f2),b1,b2)) * (i,j)) = (p1 . j) by A12, MATRIX_0:def 5;

          consider KL1 be Linear_Combination of V2 such that

           A24: ((f1 + f2) . (b1 /. i)) = ( Sum KL1) & ( Carrier KL1) c= ( rng b2) and

           A25: for t st 1 <= t & t <= ( len (((f1 + f2) . (b1 /. i)) |-- b2)) holds ((((f1 + f2) . (b1 /. i)) |-- b2) /. t) = (KL1 . (b2 /. t)) by Def7;

          b4 is linearly-independent & ((f1 + f2) . (b1 /. i)) = ((f1 . (b1 /. i)) + (f2 . (b1 /. i))) by Def3, VECTSP_7:def 3;

          

          then

           A26: (KL1 . (b2 /. j)) = ((KL2 + KL3) . (b2 /. j)) by A24, A18, A16, Th6

          .= ((KL2 . (b2 /. j)) + (KL3 . (b2 /. j))) by VECTSP_6: 22;

          

           A27: p1 = (( AutMt ((f1 + f2),b1,b2)) /. i) by A22, A20, PARTFUN1:def 6

          .= (((f1 + f2) . (b1 /. i)) |-- b2) by A21, Def8;

          consider p3 be FinSequence of K such that

           A28: p3 = (( AutMt (f2,b1,b2)) . i) and

           A29: (( AutMt (f2,b1,b2)) * (i,j)) = (p3 . j) by A15, MATRIX_0:def 5;

          consider p2 be FinSequence of K such that

           A30: p2 = (( AutMt (f1,b1,b2)) . i) and

           A31: (( AutMt (f1,b1,b2)) * (i,j)) = (p2 . j) by A14, MATRIX_0:def 5;

          

           A32: j in ( Seg ( width ( AutMt ((f1 + f2),b1,b2)))) by A13, ZFMISC_1: 87;

          then

           A33: 1 <= j by FINSEQ_1: 1;

          ( len b1) = ( len ( AutMt ((f1 + f2),b1,b2))) by Def8;

          then ( dom b1) = ( dom ( AutMt ((f1 + f2),b1,b2))) by FINSEQ_3: 29;

          then ( dom b1) <> {} by A13, ZFMISC_1: 87;

          then ( Seg ( len b1)) <> {} by FINSEQ_1:def 3;

          then ( len b1) > 0 ;

          then

           A34: j in ( Seg ( len b2)) by A32, Th39;

          then

           A35: j <= ( len b2) by FINSEQ_1: 1;

          then j <= ( len (((f1 + f2) . (b1 /. i)) |-- b2)) by Def7;

          then

           A36: (p1 /. j) = (KL1 . (b2 /. j)) by A33, A27, A25;

          

           A37: j in ( dom b2) by A34, FINSEQ_1:def 3;

          i in ( dom ( AutMt (f2,b1,b2))) by A21, Lm3;

          

          then

           A38: p3 = (( AutMt (f2,b1,b2)) /. i) by A28, PARTFUN1:def 6

          .= ((f2 . (b1 /. i)) |-- b2) by A21, Def8;

          then j in ( dom p3) by A37, Lm1;

          then

           A39: (( AutMt (f2,b1,b2)) * (i,j)) = (p3 /. j) by A29, PARTFUN1:def 6;

          i in ( dom ( AutMt (f1,b1,b2))) by A21, Lm3;

          

          then

           A40: p2 = (( AutMt (f1,b1,b2)) /. i) by A30, PARTFUN1:def 6

          .= ((f1 . (b1 /. i)) |-- b2) by A21, Def8;

          then j in ( dom p2) by A37, Lm1;

          then

           A41: (( AutMt (f1,b1,b2)) * (i,j)) = (p2 /. j) by A31, PARTFUN1:def 6;

          j <= ( len ((f2 . (b1 /. i)) |-- b2)) by A35, Def7;

          then

           A42: (p3 /. j) = (KL3 . (b2 /. j)) by A33, A38, A17;

          j <= ( len ((f1 . (b1 /. i)) |-- b2)) by A35, Def7;

          then

           A43: (p2 /. j) = (KL2 . (b2 /. j)) by A33, A40, A19;

          j in ( dom p1) by A37, A27, Lm1;

          hence thesis by A23, A41, A39, A36, A43, A42, A26, PARTFUN1:def 6;

        end;

        hence thesis by A14, MATRIX_3:def 3;

      end;

      ( len ( AutMt ((f1 + f2),b1,b2))) = ( len (( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2)))) by A1, MATRIX_3:def 3;

      hence thesis by A9, A11, MATRIX_0: 21;

    end;

    theorem :: MATRLIN:43

    a <> ( 0. K) implies ( AutMt ((a * f),b1,b2)) = (a * ( AutMt (f,b1,b2)))

    proof

      assume

       A1: a <> ( 0. K);

      

       A2: ( width ( AutMt ((a * f),b1,b2))) = ( width ( AutMt (f,b1,b2)))

      proof

        per cases ;

          suppose

           A3: ( len b1) = 0 ;

          

          then ( AutMt ((a * f),b1,b2)) = {} by Th38

          .= ( AutMt (f,b1,b2)) by A3, Th38;

          hence thesis;

        end;

          suppose

           A4: ( len b1) > 0 ;

          

          hence ( width ( AutMt ((a * f),b1,b2))) = ( len b2) by Th39

          .= ( width ( AutMt (f,b1,b2))) by A4, Th39;

        end;

      end;

      then

       A5: ( width ( AutMt ((a * f),b1,b2))) = ( width (a * ( AutMt (f,b1,b2)))) by MATRIX_3:def 5;

      

       A6: ( len ( AutMt ((a * f),b1,b2))) = ( len b1) by Def8

      .= ( len ( AutMt (f,b1,b2))) by Def8;

      then

       A7: ( dom ( AutMt ((a * f),b1,b2))) = ( dom ( AutMt (f,b1,b2))) by FINSEQ_3: 29;

      

       A8: for i, j st [i, j] in ( Indices ( AutMt ((a * f),b1,b2))) holds (( AutMt ((a * f),b1,b2)) * (i,j)) = ((a * ( AutMt (f,b1,b2))) * (i,j))

      proof

        let i, j;

        assume

         A9: [i, j] in ( Indices ( AutMt ((a * f),b1,b2)));

        then

         A10: [i, j] in [:( dom ( AutMt ((a * f),b1,b2))), ( Seg ( width ( AutMt ((a * f),b1,b2)))):] by MATRIX_0:def 4;

        then

         A11: [i, j] in ( Indices ( AutMt (f,b1,b2))) by A7, A2, MATRIX_0:def 4;

        (( AutMt ((a * f),b1,b2)) * (i,j)) = (a * (( AutMt (f,b1,b2)) * (i,j)))

        proof

          consider p2 be FinSequence of K such that

           A12: p2 = (( AutMt (f,b1,b2)) . i) and

           A13: (( AutMt (f,b1,b2)) * (i,j)) = (p2 . j) by A11, MATRIX_0:def 5;

          

           A14: i in ( dom ( AutMt ((a * f),b1,b2))) by A10, ZFMISC_1: 87;

          then

           A15: i in ( dom b1) by Lm3;

          then i in ( dom ( AutMt (f,b1,b2))) by Lm3;

          

          then

           A16: p2 = (( AutMt (f,b1,b2)) /. i) by A12, PARTFUN1:def 6

          .= ((f . (b1 /. i)) |-- b2) by A15, Def8;

          reconsider b4 = ( rng b2) as Basis of V2 by Def2;

          consider p1 be FinSequence of K such that

           A17: p1 = (( AutMt ((a * f),b1,b2)) . i) and

           A18: (( AutMt ((a * f),b1,b2)) * (i,j)) = (p1 . j) by A9, MATRIX_0:def 5;

          consider KL1 be Linear_Combination of V2 such that

           A19: ((a * f) . (b1 /. i)) = ( Sum KL1) & ( Carrier KL1) c= ( rng b2) and

           A20: for t st 1 <= t & t <= ( len (((a * f) . (b1 /. i)) |-- b2)) holds ((((a * f) . (b1 /. i)) |-- b2) /. t) = (KL1 . (b2 /. t)) by Def7;

          consider KL2 be Linear_Combination of V2 such that

           A21: (f . (b1 /. i)) = ( Sum KL2) & ( Carrier KL2) c= ( rng b2) and

           A22: for t st 1 <= t & t <= ( len ((f . (b1 /. i)) |-- b2)) holds (((f . (b1 /. i)) |-- b2) /. t) = (KL2 . (b2 /. t)) by Def7;

          b4 is linearly-independent & ((a * f) . (b1 /. i)) = (a * (f . (b1 /. i))) by Def4, VECTSP_7:def 3;

          

          then

           A23: (KL1 . (b2 /. j)) = ((a * KL2) . (b2 /. j)) by A1, A19, A21, Th7

          .= (a * (KL2 . (b2 /. j))) by VECTSP_6:def 9;

          

           A24: j in ( Seg ( width ( AutMt ((a * f),b1,b2)))) by A10, ZFMISC_1: 87;

          then

           A25: 1 <= j by FINSEQ_1: 1;

          ( len b1) = ( len ( AutMt ((a * f),b1,b2))) by Def8;

          then ( dom b1) = ( dom ( AutMt ((a * f),b1,b2))) by FINSEQ_3: 29;

          then ( dom b1) <> {} by A10, ZFMISC_1: 87;

          then ( Seg ( len b1)) <> {} by FINSEQ_1:def 3;

          then ( len b1) > 0 ;

          then

           A26: j in ( Seg ( len b2)) by A24, Th39;

          then

           A27: j <= ( len b2) by FINSEQ_1: 1;

          then j <= ( len ((f . (b1 /. i)) |-- b2)) by Def7;

          then

           A28: (p2 /. j) = (KL2 . (b2 /. j)) by A25, A16, A22;

          

           A29: j in ( dom b2) by A26, FINSEQ_1:def 3;

          then j in ( dom ((f . (b1 /. i)) |-- b2)) by Lm1;

          then

           A30: (( AutMt (f,b1,b2)) * (i,j)) = (p2 /. j) by A13, A16, PARTFUN1:def 6;

          

           A31: p1 = (( AutMt ((a * f),b1,b2)) /. i) by A17, A14, PARTFUN1:def 6

          .= (((a * f) . (b1 /. i)) |-- b2) by A15, Def8;

          then

           A32: j in ( dom p1) by A29, Lm1;

          j <= ( len (((a * f) . (b1 /. i)) |-- b2)) by A27, Def7;

          then (p1 /. j) = (KL1 . (b2 /. j)) by A25, A31, A20;

          hence thesis by A18, A32, A30, A28, A23, PARTFUN1:def 6;

        end;

        hence thesis by A11, MATRIX_3:def 5;

      end;

      ( len ( AutMt ((a * f),b1,b2))) = ( len (a * ( AutMt (f,b1,b2)))) by A6, MATRIX_3:def 5;

      hence thesis by A5, A8, MATRIX_0: 21;

    end;