theorem Th24:
for
K being
Field for
L being
Element of
K for
V1,
V2 being
finite-dimensional VectSp of
K for
b1 being
OrdBasis of
V1 for
B2 being
FinSequence of
V2 for
J being
FinSequence_of_Jordan_block of
L,
K for
M being
Matrix of
len b1,
len B2,
K st
M = block_diagonal (
J,
(0. K)) holds
for
i,
m being
Nat st
i in dom b1 &
m = min (
(Len J),
i) holds
( (
i = Sum (Len (J | m)) implies
(Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & (
i <> Sum (Len (J | m)) implies
(Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )