reconsider A' = AutMt f,B1,b2 as Matrix of len (AutMt f,B1,b2), width (AutMt f,B1,b2),K by MATRIX_2:7;
A1: len A' = len B1 by MATRLIN:def 10;

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

suppose A2: len B1 = 0 ; :: thesis: AutMt f,B1,b2 is Matrix of len B1, len b2,K

then AutMt f,B1,b2 = {} by A1;
hence AutMt f,B1,b2 is Matrix of len B1, len b2,K by A2, MATRIX_1:13; :: thesis: verum

end;

suppose len B1 > 0 ; :: thesis: AutMt f,B1,b2 is Matrix of len B1, len b2,K

then A3: ( len B1 in Seg (len B1) & dom B1 = Seg (len B1) & dom B1 = dom A' ) by A1, FINSEQ_1:5, FINSEQ_1:def 3, FINSEQ_3:31;
then (f . (B1 /. (len B1))) |-- b2 = A' /. (len B1) by MATRLIN:def 10
.= A' . (len B1) by A3, PARTFUN1:def 8
.= Line A',(len B1) by A1, A3, MATRIX_2:10 ;
then width A' = len ((f . (B1 /. (len B1))) |-- b2) by FINSEQ_1:def 18
.= len b2 by MATRLIN:def 9 ;
hence AutMt f,B1,b2 is Matrix of len B1, len b2,K by MATRLIN:def 10; :: thesis: verum

end;

end;