reconsider A' = AutMt f,B1,b2 as Matrix of the carrier of K, len (AutMt f,B1,b2), 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 the carrier of K, len B1,

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

end;

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

A4: dom B1 = dom A' 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 = A' /. (len B1) by A5, MATRLIN:def 10
.= A' . (len B1) by A3, A5, A4, FINSEQ_1:5, PARTFUN1:def 8
.= Line A',(len B1) by A1, A6, 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 the carrier of K, len B1, by MATRLIN:def 10; :: thesis: verum

end;

end;