let k, m, n be Nat; for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D holds
( Segm ((A ^^ B),(Seg n),(Seg (width A))) = A & Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B )
let D be non empty set ; for A being Matrix of n,m,D
for B being Matrix of n,k,D holds
( Segm ((A ^^ B),(Seg n),(Seg (width A))) = A & Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B )
let A be Matrix of n,m,D; for B being Matrix of n,k,D holds
( Segm ((A ^^ B),(Seg n),(Seg (width A))) = A & Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B )
let B be Matrix of n,k,D; ( Segm ((A ^^ B),(Seg n),(Seg (width A))) = A & Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B )
set AB = A ^^ B;
A1:
card (Seg n) = n
by FINSEQ_1:57;
A2:
len A = n
by MATRIX_0:def 2;
then reconsider A9 = A as Matrix of n, width A,D by MATRIX_0:51;
set S1 = Segm ((A ^^ B),(Seg n),(Seg (width A)));
A3:
card (Seg (width A)) = width A
by FINSEQ_1:57;
A4:
len (A ^^ B) = n
by MATRIX_0:def 2;
now for i, j being Nat st [i,j] in Indices A9 holds
(Segm ((A ^^ B),(Seg n),(Seg (width A)))) * (i,j) = A * (i,j)let i,
j be
Nat;
( [i,j] in Indices A9 implies (Segm ((A ^^ B),(Seg n),(Seg (width A)))) * (i,j) = A * (i,j) )assume A5:
[i,j] in Indices A9
;
(Segm ((A ^^ B),(Seg n),(Seg (width A)))) * (i,j) = A * (i,j)reconsider I =
i,
J =
j as
Element of
NAT by ORDINAL1:def 12;
A6:
dom A = Seg n
by A2, FINSEQ_1:def 3;
n <> 0
by A5, MATRIX_0:22;
then
Indices A9 = [:(Seg n),(Seg (width A)):]
by MATRIX_0:23;
then A7:
I in Seg n
by A5, ZFMISC_1:87;
A8:
J in Seg (width A)
by A5, ZFMISC_1:87;
then A9:
J =
(idseq (width A)) . J
by FINSEQ_2:49
.=
(Sgm (Seg (width A))) . J
by FINSEQ_3:48
;
dom (Segm ((A ^^ B),(Seg n),(Seg (width A)))) =
Seg (len (Segm ((A ^^ B),(Seg n),(Seg (width A)))))
by FINSEQ_1:def 3
.=
Seg n
by A1, MATRIX_0:def 2
;
hence (Segm ((A ^^ B),(Seg n),(Seg (width A)))) * (
i,
j) =
(Col ((Segm ((A ^^ B),(Seg n),(Seg (width A)))),J)) . I
by A7, MATRIX_0:def 8
.=
(Col ((A ^^ B),((Sgm (Seg (width A))) . J))) . I
by A4, A3, A8, MATRIX13:50
.=
(Col (A,J)) . I
by A8, A9, Th16
.=
A * (
i,
j)
by A7, A6, MATRIX_0:def 8
;
verum end;
hence
A = Segm ((A ^^ B),(Seg n),(Seg (width A)))
by A1, A3, MATRIX_0:27; Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B
set w = (width A) + (width B);
set SS = (Seg ((width A) + (width B))) \ (Seg (width A));
set S2 = Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))));
A10:
len B = n
by MATRIX_0:def 2;
then reconsider B9 = B as Matrix of n, width B,D by MATRIX_0:51;
width A <= (width A) + (width B)
by NAT_1:11;
then
( card (Seg ((width A) + (width B))) = (width A) + (width B) & Seg (width A) c= Seg ((width A) + (width B)) )
by FINSEQ_1:5, FINSEQ_1:57;
then A11: card ((Seg ((width A) + (width B))) \ (Seg (width A))) =
((width A) + (width B)) - (width A)
by A3, CARD_2:44
.=
width B
;
now for i, j being Nat st [i,j] in Indices B9 holds
(Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))) * (i,j) = B9 * (i,j)A12:
dom B = Seg n
by A10, FINSEQ_1:def 3;
let i,
j be
Nat;
( [i,j] in Indices B9 implies (Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))) * (i,j) = B9 * (i,j) )assume A13:
[i,j] in Indices B9
;
(Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))) * (i,j) = B9 * (i,j)reconsider I =
i,
J =
j as
Element of
NAT by ORDINAL1:def 12;
A14:
J in Seg (width B)
by A13, ZFMISC_1:87;
n <> 0
by A13, MATRIX_0:22;
then
Indices B9 = [:(Seg n),(Seg (width B)):]
by MATRIX_0:23;
then A15:
I in Seg n
by A13, ZFMISC_1:87;
dom (Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))) =
Seg (len (Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))))
by FINSEQ_1:def 3
.=
Seg n
by A1, MATRIX_0:def 2
;
hence (Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))) * (
i,
j) =
(Col ((Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))))),J)) . I
by A15, MATRIX_0:def 8
.=
(Col ((A ^^ B),((Sgm ((Seg ((width A) + (width B))) \ (Seg (width A)))) . J))) . I
by A4, A11, A14, MATRIX13:50
.=
(Col ((A ^^ B),((width A) + J))) . I
by A14, Th8
.=
(Col (B,J)) . I
by A14, Th17
.=
B9 * (
i,
j)
by A15, A12, MATRIX_0:def 8
;
verum end;
hence
Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B
by A1, A11, MATRIX_0:27; verum