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 A5:
N > 0
;
A ^^ B is Matrix of n,(width A) + (width B),Dthen 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;
verum end; end;