reconsider A9 = AutMt (f,B1,b2) as Matrix of len (AutMt (f,B1,b2)), width (AutMt (f,B1,b2)),K by MATRIX_0:51;
A1: len A9 = len B1 by MATRLIN:def 8;

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_0: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:29;
A5: dom B1 = Seg (len B1) by FINSEQ_1:def 3;
A6: len B1 in Seg (len B1) by A3, FINSEQ_1:3;
then (f . (B1 /. (len B1))) |-- b2 = A9 /. (len B1) by A5, MATRLIN:def 8
.= A9 . (len B1) by A3, A5, A4, FINSEQ_1:3, PARTFUN1:def 6
.= Line (A9,(len B1)) by A1, A6, MATRIX_0:52 ;
then A7: width A9 = len ((f . (B1 /. (len B1))) |-- b2) by CARD_1:def 7
.= len b2 by MATRLIN:def 7 ;
len A9 = len B1 by MATRLIN:def 8;
hence AutMt (f,B1,b2) is Matrix of len B1, len b2,K by A7; :: thesis: verum

end;

end;