reconsider A9 = AutMt f,B1,b2 as Matrix of len (AutMt f,B1,b2), width (AutMt f,B1,b2),K by MATRIX_2:7;
A1: len A9 = 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 A3: len B1 > 0 ; :: thesis: AutMt f,B1,b2 is Matrix of len B1, len b2,K

A4: dom B1 = dom A9 by A1, FINSEQ_3:31;
A5: dom B1 = Seg (len B1) by FINSEQ_1:def 3;
A6: len B1 in Seg (len B1) by A3, FINSEQ_1:5;
then (f . (B1 /. (len B1))) |-- b2 = A9 /. (len B1) by A5, MATRLIN:def 10
.= A9 . (len B1) by A3, A5, A4, FINSEQ_1:5, PARTFUN1:def 8
.= Line A9,(len B1) by A1, A6, MATRIX_2:10 ;
then width A9 = 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;