reconsider N = n as Element of NAT by ORDINAL1:def 13;
set AB = A ^^ B;
A1: dom B = Seg (len B) by FINSEQ_1:def 3
.= Seg n by MATRIX_1:def 3 ;
dom A = Seg (len A) by FINSEQ_1:def 3
.= Seg n by MATRIX_1:def 3 ;
then A2: dom (A ^^ B) = (Seg n) /\ (Seg n) by A1, PRE_POLY:def 4
.= Seg n ;
then A3: len (A ^^ B) = N by FINSEQ_1:def 3;

per cases ( N = 0 or N > 0 ) ;

suppose A4: N = 0 ; :: thesis: A ^^ B is Matrix of n,(width A) + (width B),D

then A ^^ B = {} by A2;
hence A ^^ B is Matrix of n,(width A) + (width B),D by A4, MATRIX_1:13; :: thesis: verum

end;

suppose A5: N > 0 ; :: thesis: A ^^ B is Matrix of n,(width A) + (width B),D

then A6: N in Seg N by FINSEQ_1:5;
then ( A . N = Line A,N & B . N = Line B,N ) by MATRIX_2:10;
then A7: (A ^^ B) . N = (Line A,N) ^ (Line B,N) by A2, A6, PRE_POLY:def 4;
A8: len ((Line A,N) ^ (Line B,N)) = (width A) + (width B) by FINSEQ_1:def 18;
(A ^^ B) . N in rng (A ^^ B) by A2, A6, FUNCT_1:def 5;
then width (A ^^ B) = (width A) + (width B) by A3, A5, A7, A8, MATRIX_1:def 4;
hence A ^^ B is Matrix of n,(width A) + (width B),D by A3, MATRIX_2:7; :: thesis: verum

end;

end;