set B = <*b*>;
A1: len <*b*> = 1 by MATRIX_0:23;
A2: width <*b*> = len b by MATRIX_0:23;
A3: len (<*b*> @) = width <*b*> by MATRIX_0:def 6;

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_0:23;
hence <*b*> @ is Matrix of len b,1,D by A4, MATRIX_0: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_0:54;
hence <*b*> @ is Matrix of len b,1,D by A1, A2, A3, MATRIX_0:51; :: thesis: verum

end;

end;