theorem Th23: :: MATRIXJ2:23

for n being Nat
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 M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds
for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )