:: MATRLIN semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let A, X be set ;
let D be FinSequence-DOMAIN of A;
let p be PartFunc of X,D;
let i be set ;
:: original: /.
redefine func p /. i -> Element of D;
coherence
p /. i is Element of D
;
end;

theorem :: MATRLIN:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MATRLIN:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

definition
let D be non empty set ;
let k be Nat;
let M be Matrix of D;
:: original: Del
redefine func Del M,k -> Matrix of D;
coherence
Del M,k is Matrix of D
proof end;
end;

theorem Th3: :: MATRLIN:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for M being FinSequence st len M = n + 1 holds
len (Del M,(n + 1)) = n
proof end;

theorem Th4: :: MATRLIN:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for D being non empty set
for M being Matrix of n + 1,m,D
for M1 being Matrix of D holds
( ( n > 0 implies width M = width (Del M,(n + 1)) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) )
proof end;

theorem Th5: :: MATRLIN:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for D being non empty set
for M being Matrix of n + 1,m,D holds Del M,(n + 1) is Matrix of n,m,D
proof end;

theorem Th6: :: MATRLIN:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for M being FinSequence st len M = n + 1 holds
M = (Del M,(len M)) ^ <*(M . (len M))*>
proof end;

definition
let D be non empty set ;
let P be FinSequence of D;
:: original: <*
redefine func <*P*> -> Matrix of 1, len P,D;
coherence
<*P*> is Matrix of 1, len P,D
by MATRIX_1:11;
end;

theorem Th7: :: MATRLIN:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for F being FinSequence holds (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of dom F
proof end;

theorem Th8: :: MATRLIN:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being FinSequence
for A being Subset of (rng F) st F is one-to-one holds
ex p being Permutation of dom F st (F - (A ` )) ^ (F - A) = F * p
proof end;

definition
let IT be Function;
attr IT is FinSequence-yielding means :Def1: :: MATRLIN:def 1
for x being set st x in dom IT holds
IT . x is FinSequence;
end;

:: deftheorem Def1 defines FinSequence-yielding MATRLIN:def 1 :
for IT being Function holds
( IT is FinSequence-yielding iff for x being set st x in dom IT holds
IT . x is FinSequence );

registration
cluster FinSequence-yielding set ;
existence
ex b1 being Function st b1 is FinSequence-yielding
proof end;
end;

definition
let F, G be FinSequence-yielding Function;
func F ^^ G -> FinSequence-yielding Function means :Def2: :: MATRLIN:def 2
( dom it = (dom F) /\ (dom G) & ( for i being set st i in dom it holds
for f, g being FinSequence st f = F . i & g = G . i holds
it . i = f ^ g ) );
existence
ex b1 being FinSequence-yielding Function st
( dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds
for f, g being FinSequence st f = F . i & g = G . i holds
b1 . i = f ^ g ) )
proof end;
uniqueness
for b1, b2 being FinSequence-yielding Function st dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds
for f, g being FinSequence st f = F . i & g = G . i holds
b1 . i = f ^ g ) & dom b2 = (dom F) /\ (dom G) & ( for i being set st i in dom b2 holds
for f, g being FinSequence st f = F . i & g = G . i holds
b2 . i = f ^ g ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ^^ MATRLIN:def 2 :
for F, G, b3 being FinSequence-yielding Function holds
( b3 = F ^^ G iff ( dom b3 = (dom F) /\ (dom G) & ( for i being set st i in dom b3 holds
for f, g being FinSequence st f = F . i & g = G . i holds
b3 . i = f ^ g ) ) );

theorem Th9: :: MATRLIN:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V being VectSp of K
for KL1, KL2 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds
KL1 = KL2
proof end;

theorem Th10: :: MATRLIN:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V being VectSp of K
for KL1, KL2, KL3 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds
KL1 = KL2 + KL3
proof end;

theorem Th11: :: MATRLIN:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V being VectSp of K
for a being Element of K
for KL1, KL2 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) holds
KL1 = a * KL2
proof end;

theorem Th12: :: MATRLIN:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V being VectSp of K
for W being Element of V
for b2 being Basis of V ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= b2 )
proof end;

definition
let K be Field;
let V be VectSp of K;
attr V is finite-dimensional means :Def3: :: MATRLIN:def 3
ex A being finite Subset of V st A is Basis of V;
end;

:: deftheorem Def3 defines finite-dimensional MATRLIN:def 3 :
for K being Field
for V being VectSp of K holds
( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );

registration
let K be Field;
cluster strict finite-dimensional VectSpStr of K;
existence
ex b1 being VectSp of K st
( b1 is strict & b1 is finite-dimensional )
proof end;
end;

definition
let K be Field;
let V be finite-dimensional VectSp of K;
mode OrdBasis of V -> FinSequence of the carrier of V means :Def4: :: MATRLIN:def 4
( it is one-to-one & rng it is Basis of V );
existence
ex b1 being FinSequence of the carrier of V st
( b1 is one-to-one & rng b1 is Basis of V )
proof end;
end;

:: deftheorem Def4 defines OrdBasis MATRLIN:def 4 :
for K being Field
for V being finite-dimensional VectSp of K
for b3 being FinSequence of the carrier of V holds
( b3 is OrdBasis of V iff ( b3 is one-to-one & rng b3 is Basis of V ) );

Lm1: for p, s being FinSequence st len p = len s & ( for j being Nat st j in dom p holds
p . j = s . j ) holds
p = s
proof end;

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V1, V2 be VectSp of K;
let f1, f2 be Function of V1,V2;
func f1 + f2 -> Function of V1,V2 means :Def5: :: MATRLIN:def 5
for v being Element of V1 holds it . v = (f1 . v) + (f2 . v);
existence
ex b1 being Function of V1,V2 st
for v being Element of V1 holds b1 . v = (f1 . v) + (f2 . v)
proof end;
uniqueness
for b1, b2 being Function of V1,V2 st ( for v being Element of V1 holds b1 . v = (f1 . v) + (f2 . v) ) & ( for v being Element of V1 holds b2 . v = (f1 . v) + (f2 . v) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines + MATRLIN:def 5 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V1, V2 being VectSp of K
for f1, f2, b6 being Function of V1,V2 holds
( b6 = f1 + f2 iff for v being Element of V1 holds b6 . v = (f1 . v) + (f2 . v) );

definition
let K be Field;
let V1, V2 be finite-dimensional VectSp of K;
let f be Function of V1,V2;
let a be Element of K;
func a * f -> Function of V1,V2 means :Def6: :: MATRLIN:def 6
for v being Element of V1 holds it . v = a * (f . v);
existence
ex b1 being Function of V1,V2 st
for v being Element of V1 holds b1 . v = a * (f . v)
proof end;
uniqueness
for b1, b2 being Function of V1,V2 st ( for v being Element of V1 holds b1 . v = a * (f . v) ) & ( for v being Element of V1 holds b2 . v = a * (f . v) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines * MATRLIN:def 6 :
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for a being Element of K
for b6 being Function of V1,V2 holds
( b6 = a * f iff for v being Element of V1 holds b6 . v = a * (f . v) );

theorem Th13: :: MATRLIN:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for a being Element of V1
for F being FinSequence of the carrier of V1
for G being FinSequence of the carrier of K st len F = len G & ( for k being Nat
for v being Element of K st k in dom F & v = G . k holds
F . k = v * a ) holds
Sum F = (Sum G) * a
proof end;

theorem Th14: :: MATRLIN:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for a being Element of V1
for F being FinSequence of the carrier of K
for G being FinSequence of the carrier of V1 st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
proof end;

theorem Th15: :: MATRLIN:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V1 being non empty add-associative right_zeroed right_complementable LoopStr
for F being FinSequence of the carrier of V1 st ( for k being Nat st k in dom F holds
F /. k = 0. V1 ) holds
Sum F = 0. V1
proof end;

definition
let K be Field;
let V1 be finite-dimensional VectSp of K;
let p1 be FinSequence of the carrier of K;
let p2 be FinSequence of the carrier of V1;
func lmlt p1,p2 -> FinSequence of the carrier of V1 equals :: MATRLIN:def 7
the lmult of V1 .: p1,p2;
coherence
the lmult of V1 .: p1,p2 is FinSequence of the carrier of V1
;
end;

:: deftheorem defines lmlt MATRLIN:def 7 :
for K being Field
for V1 being finite-dimensional VectSp of K
for p1 being FinSequence of the carrier of K
for p2 being FinSequence of the carrier of V1 holds lmlt p1,p2 = the lmult of V1 .: p1,p2;

theorem Th16: :: MATRLIN:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for p2 being FinSequence of the carrier of V1
for p1 being FinSequence of the carrier of K st dom p1 = dom p2 holds
dom (lmlt p1,p2) = dom p1
proof end;

definition
let V1 be non empty LoopStr ;
let M be FinSequence of the carrier of V1 * ;
func Sum M -> FinSequence of the carrier of V1 means :Def8: :: MATRLIN:def 8
( len it = len M & ( for k being Nat st k in dom it holds
it /. k = Sum (M /. k) ) );
existence
ex b1 being FinSequence of the carrier of V1 st
( len b1 = len M & ( for k being Nat st k in dom b1 holds
b1 /. k = Sum (M /. k) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of V1 st len b1 = len M & ( for k being Nat st k in dom b1 holds
b1 /. k = Sum (M /. k) ) & len b2 = len M & ( for k being Nat st k in dom b2 holds
b2 /. k = Sum (M /. k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Sum MATRLIN:def 8 :
for V1 being non empty LoopStr
for M being FinSequence of the carrier of V1 *
for b3 being FinSequence of the carrier of V1 holds
( b3 = Sum M iff ( len b3 = len M & ( for k being Nat st k in dom b3 holds
b3 /. k = Sum (M /. k) ) ) );

theorem Th17: :: MATRLIN:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for M being Matrix of the carrier of V1 st len M = 0 holds
Sum (Sum M) = 0. V1
proof end;

theorem Th18: :: MATRLIN:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for M being Matrix of m + 1,0,the carrier of V1 holds Sum (Sum M) = 0. V1
proof end;

theorem Th19: :: MATRLIN:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for x being Element of V1 holds <*<*x*>*> = <*<*x*>*> @
proof end;

theorem Th20: :: MATRLIN:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V2, V1 being finite-dimensional VectSp of K
for f being Function of V1,V2
for p being FinSequence of the carrier of V1 st f is linear holds
f . (Sum p) = Sum (f * p)
proof end;

theorem Th21: :: MATRLIN:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V2, V1 being finite-dimensional VectSp of K
for f being Function of V1,V2
for a being FinSequence of the carrier of K
for p being FinSequence of the carrier of V1 st len p = len a & f is linear holds
f * (lmlt a,p) = lmlt a,(f * p)
proof end;

theorem Th22: :: MATRLIN:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V3, V2 being finite-dimensional VectSp of K
for g being Function of V2,V3
for b2 being OrdBasis of V2
for a being FinSequence of the carrier of K st len a = len b2 & g is linear holds
g . (Sum (lmlt a,b2)) = Sum (lmlt a,(g * b2))
proof end;

theorem Th23: :: MATRLIN:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for F, F1 being FinSequence of the carrier of V1
for KL being Linear_Combination of V1
for p being Permutation of dom F st F1 = F * p holds
KL (#) F1 = (KL (#) F) * p
proof end;

theorem Th24: :: MATRLIN:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for F being FinSequence of the carrier of V1
for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds
Sum (KL (#) F) = Sum KL
proof end;

theorem Th25: :: MATRLIN:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V2, V1 being finite-dimensional VectSp of K
for f1, f2 being Function of V1,V2
for A being set
for p being FinSequence of the carrier of V1 st rng p c= A & f1 is linear & f2 is linear & ( for v being Element of V1 st v in A holds
f1 . v = f2 . v ) holds
f1 . (Sum p) = f2 . (Sum p)
proof end;

theorem Th26: :: MATRLIN:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V2, V1 being finite-dimensional VectSp of K
for f1, f2 being Function of V1,V2 st f1 is linear & f2 is linear holds
for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds
f1 = f2
proof end;

registration
let D be non empty set ;
cluster -> FinSequence-yielding FinSequence of D * ;
coherence
for b1 being Matrix of D holds b1 is FinSequence-yielding
proof end;
end;

definition
let D be non empty set ;
let F, G be Matrix of D;
:: original: ^^
redefine func F ^^ G -> Matrix of D;
coherence
F ^^ G is Matrix of D
proof end;
end;

definition
let D be non empty set ;
let n, m, k be Nat;
let M1 be Matrix of n,k,D;
let M2 be Matrix of m,k,D;
:: original: ^
redefine func M1 ^ M2 -> Matrix of n + m,k,D;
coherence
M1 ^ M2 is Matrix of n + m,k,D
proof end;
end;

theorem :: MATRLIN:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k, m, i being Nat
for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st i in dom M1 holds
Line (M1 ^ M2),i = Line M1,i
proof end;

theorem Th28: :: MATRLIN:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k, m being Nat
for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
width (M1 ^ M2) = width M1
proof end;

theorem :: MATRLIN:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t, k, m, n, i being Nat
for D being non empty set
for M1 being Matrix of t,k,D
for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds
Line (M1 ^ M2),i = Line M2,n
proof end;

theorem Th30: :: MATRLIN:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k, m being Nat
for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
for i being Nat st i in Seg (width M1) holds
Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i)
proof end;

theorem Th31: :: MATRLIN:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k, m being Nat
for K being Field
for V being VectSp of K
for M1 being Matrix of n,k,the carrier of V
for M2 being Matrix of m,k,the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
proof end;

theorem Th32: :: MATRLIN:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k, m being Nat
for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
(M1 ^ M2) @ = (M1 @ ) ^^ (M2 @ )
proof end;

theorem Th33: :: MATRLIN:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for M1, M2 being Matrix of the carrier of V1 holds the add of V1 .: (Sum M1),(Sum M2) = Sum (M1 ^^ M2)
proof end;

definition
let D be non empty set ;
let F be BinOp of D;
let P1, P2 be FinSequence of D;
:: original: .:
redefine func F .: P1,P2 -> FinSequence of D;
coherence
F .: P1,P2 is FinSequence of D
proof end;
end;

theorem Th34: :: MATRLIN:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for P1, P2 being FinSequence of the carrier of V1 st len P1 = len P2 holds
Sum (the add of V1 .: P1,P2) = (Sum P1) + (Sum P2)
proof end;

theorem Th35: :: MATRLIN:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds
(Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2))
proof end;

theorem :: MATRLIN:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th37: :: MATRLIN:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @ ))
proof end;

theorem Th38: :: MATRLIN:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for M being Matrix of n,m,the carrier of K st n > 0 & m > 0 holds
for p, d being FinSequence of the carrier of K st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt p,(Col M,j)) ) holds
for b, c being FinSequence of the carrier of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt (Line M,i),b) ) holds
Sum (lmlt p,c) = Sum (lmlt d,b)
proof end;

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;
func W |-- b1 -> FinSequence of the carrier of K means :Def9: :: MATRLIN:def 9
( len it = len b1 & ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len it holds
it /. k = KL . (b1 /. k) ) ) );
existence
ex b1 being FinSequence of the carrier of K st
( len b1 = len b1 & ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b1 holds
b1 /. k = KL . (b1 /. k) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of K st len b1 = len b1 & ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b1 holds
b1 /. k = KL . (b1 /. k) ) ) & len b2 = len b1 & ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b2 holds
b2 /. k = KL . (b1 /. k) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines |-- MATRLIN:def 9 :
for K being Field
for V being finite-dimensional VectSp of K
for b1 being OrdBasis of V
for W being Element of V
for b5 being FinSequence of the carrier of K holds
( b5 = W |-- b1 iff ( len b5 = len b1 & ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b5 holds
b5 /. k = KL . (b1 /. k) ) ) ) );

Lm2: for K being Field
for V being finite-dimensional VectSp of K
for b being OrdBasis of V
for W being Element of V holds dom (W |-- b) = dom b
proof end;

theorem Th39: :: MATRLIN:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V2 being finite-dimensional VectSp of K
for b2 being OrdBasis of V2
for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds
v1 = v2
proof end;

theorem Th40: :: MATRLIN:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v being Element of V1 holds v = Sum (lmlt (v |-- b1),b1)
proof end;

theorem Th41: :: MATRLIN:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for d being FinSequence of the carrier of K st len d = len b1 holds
d = (Sum (lmlt d,b1)) |-- b1
proof end;

Lm3: for p being FinSequence
for k being set st k in dom p holds
len p > 0
proof end;

theorem Th42: :: MATRLIN:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V2, V3 being finite-dimensional VectSp of K
for g being Function of V2,V3
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3
for a, d being FinSequence of the carrier of K st len a = len b2 holds
for j being Nat st j in dom b3 & len d = len b2 & ( for k being Nat st k in dom b2 holds
d . k = ((g . (b2 /. k)) |-- b3) /. j ) & len b2 > 0 holds
((Sum (lmlt a,(g * b2))) |-- b3) /. j = Sum (mlt a,d)
proof end;

definition
let K be Field;
let V1, V2 be finite-dimensional VectSp of K;
let f be Function of the carrier of V1,the carrier of V2;
let b1 be FinSequence of the carrier of V1;
let b2 be OrdBasis of V2;
func AutMt f,b1,b2 -> Matrix of K means :Def10: :: MATRLIN:def 10
( len it = len b1 & ( for k being Nat st k in dom b1 holds
it /. k = (f . (b1 /. k)) |-- b2 ) );
existence
ex b1 being Matrix of K st
( len b1 = len b1 & ( for k being Nat st k in dom b1 holds
b1 /. k = (f . (b1 /. k)) |-- b2 ) )
proof end;
uniqueness
for b1, b2 being Matrix of K st len b1 = len b1 & ( for k being Nat st k in dom b1 holds
b1 /. k = (f . (b1 /. k)) |-- b2 ) & len b2 = len b1 & ( for k being Nat st k in dom b1 holds
b2 /. k = (f . (b1 /. k)) |-- b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines AutMt MATRLIN:def 10 :
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of the carrier of V1,the carrier of V2
for b1 being FinSequence of the carrier of V1
for b2 being OrdBasis of V2
for b7 being Matrix of K holds
( b7 = AutMt f,b1,b2 iff ( len b7 = len b1 & ( for k being Nat st k in dom b1 holds
b7 /. k = (f . (b1 /. k)) |-- b2 ) ) );

Lm4: for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds dom (AutMt f,b1,b2) = dom b1
proof end;

theorem Th43: :: MATRLIN:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st len b1 = 0 holds
AutMt f,b1,b2 = {}
proof end;

theorem Th44: :: MATRLIN:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st len b1 > 0 holds
width (AutMt f,b1,b2) = len b2
proof end;

theorem :: MATRLIN:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f1, f2 being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st f1 is linear & f2 is linear & AutMt f1,b1,b2 = AutMt f2,b1,b2 & len b1 > 0 holds
f1 = f2
proof end;

theorem :: MATRLIN:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1, V2, V3 being finite-dimensional VectSp of K
for f being Function of V1,V2
for g being Function of V2,V3
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V3 st f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 holds
AutMt (g * f),b1,b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
proof end;

theorem :: MATRLIN:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f1, f2 being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds AutMt (f1 + f2),b1,b2 = (AutMt f1,b1,b2) + (AutMt f2,b1,b2)
proof end;

theorem :: MATRLIN:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for a being Element of K
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st a <> 0. K holds
AutMt (a * f),b1,b2 = a * (AutMt f,b1,b2)
proof end;