theorem Th19:
for
i being
Nat for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
K for
W1,
W2 being
Subspace of
V1 for
U1,
U2 being
Subspace of
V2 for
b1 being
OrdBasis of
V1 for
B2 being
FinSequence of
V2 for
bw1 being
OrdBasis of
W1 for
bw2 being
OrdBasis of
W2 for
Bu1 being
FinSequence of
U1 for
Bu2 being
FinSequence of
U2 for
M being
Matrix of
len b1,
len B2,
K for
M1 being
Matrix of
len bw1,
len Bu1,
K for
M2 being
Matrix of
len bw2,
len Bu2,
K st
b1 = bw1 ^ bw2 &
B2 = Bu1 ^ Bu2 &
M = block_diagonal (
<*M1,M2*>,
(0. K)) &
width M1 = len Bu1 &
width M2 = len Bu2 holds
( (
i in dom bw1 implies
(Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & (
i in dom bw2 implies
(Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )