theorem Th20:
for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
K for
b1 being
OrdBasis of
V1 for
B2 being
FinSequence of
V2 for
M being
Matrix of
len b1,
len B2,
K for
F being
FinSequence_of_Matrix of
K st
M = block_diagonal (
F,
(0. K)) holds
for
i,
m being
Nat st
i in dom b1 &
m = min (
(Len F),
i) holds
(
(Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) &
len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )