( len (Jordan_block (L,n)) = n & width (Jordan_block (L,n)) = n ) by Def1;
then reconsider LBn = Jordan_block (L,n) as Matrix of n,K by MATRIX_0:51;
now :: thesis: for i, j being Nat st [i,j] in Indices LBn & i > j holds
LBn * (i,j) = 0. K
let i, j be Nat; :: thesis: ( [i,j] in Indices LBn & i > j implies LBn * (i,j) = 0. K )
assume A1: [i,j] in Indices LBn ; :: thesis: ( i > j implies LBn * (i,j) = 0. K )
assume A2: i > j ; :: thesis: LBn * (i,j) = 0. K
then i + 1 > j by NAT_1:13;
hence LBn * (i,j) = 0. K by A1, A2, Def1; :: thesis: verum
end;
hence Jordan_block (L,n) is upper_triangular Matrix of n,K by MATRIX_1:def 8; :: thesis: verum