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

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

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

then <*b*> @ = {} by A3, MATRIX_1:24;
hence <*b*> @ is Matrix of len b,1,D by A4, 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 A2, MATRIX_2:12;
hence <*b*> @ is Matrix of len b,1,D by A1, A2, A3, MATRIX_2:7; :: thesis: verum

end;

end;