reconsider N = n as Element of NAT by ORDINAL1:def 12;

set AB = A ^^ B;

A1: dom B = Seg (len B) by FINSEQ_1:def 3

.= Seg n by MATRIX_0:def 2 ;

dom A = Seg (len A) by FINSEQ_1:def 3

.= Seg n by MATRIX_0:def 2 ;

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;

set AB = A ^^ B;

A1: dom B = Seg (len B) by FINSEQ_1:def 3

.= Seg n by MATRIX_0:def 2 ;

dom A = Seg (len A) by FINSEQ_1:def 3

.= Seg n by MATRIX_0:def 2 ;

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 )
;

end;

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_0:13; :: thesis: verum

end;hence A ^^ B is Matrix of n,(width A) + (width B),D by A4, MATRIX_0:13; :: thesis: verum

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:3;

then ( A . N = Line (A,N) & B . N = Line (B,N) ) by MATRIX_0:52;

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 CARD_1:def 7;

(A ^^ B) . N in rng (A ^^ B) by A2, A6, FUNCT_1:def 3;

then width (A ^^ B) = (width A) + (width B) by A3, A5, A7, A8, MATRIX_0:def 3;

hence A ^^ B is Matrix of n,(width A) + (width B),D by A3, MATRIX_0:51; :: thesis: verum

end;then ( A . N = Line (A,N) & B . N = Line (B,N) ) by MATRIX_0:52;

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 CARD_1:def 7;

(A ^^ B) . N in rng (A ^^ B) by A2, A6, FUNCT_1:def 3;

then width (A ^^ B) = (width A) + (width B) by A3, A5, A7, A8, MATRIX_0:def 3;

hence A ^^ B is Matrix of n,(width A) + (width B),D by A3, MATRIX_0:51; :: thesis: verum