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;

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;