let n, m, k be Nat; :: thesis: for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D
for i being Nat st i in Seg (width B) holds
Col (A ^^ B),((width A) + i) = Col B,i
let D be non empty set ; :: thesis: for A being Matrix of n,m,D
for B being Matrix of n,k,D
for i being Nat st i in Seg (width B) holds
Col (A ^^ B),((width A) + i) = Col B,i
let A be Matrix of n,m,D; :: thesis: for B being Matrix of n,k,D
for i being Nat st i in Seg (width B) holds
Col (A ^^ B),((width A) + i) = Col B,i
let B be Matrix of n,k,D; :: thesis: for i being Nat st i in Seg (width B) holds
Col (A ^^ B),((width A) + i) = Col B,i
let i be Nat; :: thesis: ( i in Seg (width B) implies Col (A ^^ B),((width A) + i) = Col B,i )
assume A1:
i in Seg (width B)
; :: thesis: Col (A ^^ B),((width A) + i) = Col B,i
set AB = A ^^ B;
A2:
( len B = n & len (A ^^ B) = n )
by MATRIX_1:def 3;
now let j be
Nat;
:: thesis: ( j in Seg n implies (Col (A ^^ B),((width A) + i)) . j = (Col B,i) . j )assume A3:
j in Seg n
;
:: thesis: (Col (A ^^ B),((width A) + i)) . j = (Col B,i) . jA4:
(
dom (A ^^ B) = Seg n &
dom B = Seg n )
by A2, FINSEQ_1:def 3;
n <> 0
by A3;
then
n > 0
;
then
width (A ^^ B) = (width A) + (width B)
by MATRIX_1:24;
then A5:
(width A) + i in Seg (width (A ^^ B))
by A1, FINSEQ_1:81;
A6:
(
dom (Line B,j) = Seg (width B) &
len (Line A,j) = width A )
by FINSEQ_1:def 18, FINSEQ_2:144;
thus (Col (A ^^ B),((width A) + i)) . j =
(A ^^ B) * j,
((width A) + i)
by A3, A4, MATRIX_1:def 9
.=
(Line (A ^^ B),j) . ((width A) + i)
by A5, MATRIX_1:def 8
.=
((Line A,j) ^ (Line B,j)) . ((width A) + i)
by Th15, A3
.=
(Line B,j) . i
by A1, A6, FINSEQ_1:def 7
.=
B * j,
i
by A1, MATRIX_1:def 8
.=
(Col B,i) . j
by A3, A4, MATRIX_1:def 9
;
:: thesis: verum end;
hence
Col (A ^^ B),((width A) + i) = Col B,i
by A2, FINSEQ_2:139; :: thesis: verum