theorem
for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
K for
b1 being
OrdBasis of
V1 for
b2 being
OrdBasis of
V2 for
f being
linear-transformation of
V1,
V2 for
W1,
W2 being
Subspace of
V1 for
U1,
U2 being
Subspace of
V2 st (
dim W1 = 0 implies
dim U1 = 0 ) & (
dim W2 = 0 implies
dim U2 = 0 ) &
V2 is_the_direct_sum_of U1,
U2 holds
for
fW1 being
linear-transformation of
W1,
U1 for
fW2 being
linear-transformation of
W2,
U2 st
fW1 = f | W1 &
fW2 = f | W2 holds
for
w1 being
OrdBasis of
W1 for
w2 being
OrdBasis of
W2 for
u1 being
OrdBasis of
U1 for
u2 being
OrdBasis of
U2 st
w1 ^ w2 = b1 &
u1 ^ u2 = b2 holds
AutMt (
f,
b1,
b2)
= block_diagonal (
<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,
(0. K))