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 A1: F = {} ; :: thesis: block_diagonal F,d = {}
len (Len F) = 0 by A1, FINSEQ_1:def 18;
then Len F = <*> REAL ;
then 0 = len (block_diagonal F,d) by Def5, RVSUM_1:102;
hence block_diagonal F,d = {} ; :: thesis: verum