let D be non empty set ; :: thesis: for d being Element of D
for F being FinSequence_of_Matrix of D st F = {} holds
block_diagonal (F,d) = {}
let d be Element of D; :: thesis: for F being FinSequence_of_Matrix of D st F = {} holds
block_diagonal (F,d) = {}
let F be FinSequence_of_Matrix of D; :: thesis: ( F = {} implies block_diagonal (F,d) = {} )
assume F = {} ; :: thesis: block_diagonal (F,d) = {}
then len (Len F) = 0 ;
then Len F = <*> REAL ;
then 0 = len (block_diagonal (F,d)) by Def5, RVSUM_1:72;
hence block_diagonal (F,d) = {} ; :: thesis: verum