set B = <*b*>;
A1: ( len <*b*> = 1 & width <*b*> = len b & len (<*b*> @ ) = width <*b*> ) by MATRIX_1:24, MATRIX_1:def 7;

per cases ( len b = 0 or len b > 0 ) ;

suppose A2: len b = 0 ; :: thesis: <*b*> @ is Matrix of len b,1,D

then <*b*> @ = {} by A1;
hence <*b*> @ is Matrix of len b,1,D by A2, MATRIX_1:13; :: thesis: verum

end;

suppose len b > 0 ; :: thesis: <*b*> @ is Matrix of len b,1,D

then width (<*b*> @ ) = len <*b*> by A1, MATRIX_2:12;
hence <*b*> @ is Matrix of len b,1,D by A1, MATRIX_2:7; :: thesis: verum

end;

end;