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;
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_0: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: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;
end;