begin
begin
begin
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;
^redefine func M1 ^ M2 -> Matrix of
n + m,
k,
D;
coherence
M1 ^ M2 is Matrix of n + m,k,D
end;
theorem
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)
theorem Th33:
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
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
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))
begin
Lm1:
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
Lm2:
for p being FinSequence
for k being set st k in dom p holds
len p > 0
begin
Lm3:
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
theorem
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
g is
additive &
g is
homogeneous &
len b1 > 0 &
len b2 > 0 holds
AutMt (
(g * f),
b1,
b3)
= (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))