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 A) holds
Col (A ^^ B),i = Col A,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 A) holds
Col (A ^^ B),i = Col A,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 A) holds
Col (A ^^ B),i = Col A,i
let B be Matrix of n,k,D; :: thesis: for i being Nat st i in Seg (width A) holds
Col (A ^^ B),i = Col A,i
let i be Nat; :: thesis: ( i in Seg (width A) implies Col (A ^^ B),i = Col A,i )
assume A1: i in Seg (width A) ; :: thesis: Col (A ^^ B),i = Col A,i
set AB = A ^^ B;
A2: ( len A = n & len (A ^^ B) = n ) by MATRIX_1:def 3;

now

let j be Nat; :: thesis: ( j in Seg n implies (Col (A ^^ B),i) . j = (Col A,i) . j )
assume A3: j in Seg n ; :: thesis: (Col (A ^^ B),i) . j = (Col A,i) . j
A4: ( dom (A ^^ B) = Seg n & dom A = 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 width A <= width (A ^^ B) by NAT_1:11;
then A5: Seg (width A) c= Seg (width (A ^^ B)) by FINSEQ_1:7;
A6: dom (Line A,j) = Seg (width A) by FINSEQ_2:144;
thus (Col (A ^^ B),i) . j = (A ^^ B) * j,i by A3, A4, MATRIX_1:def 9
.= (Line (A ^^ B),j) . i by A1, A5, MATRIX_1:def 8
.= ((Line A,j) ^ (Line B,j)) . i by Th15, A3
.= (Line A,j) . i by A1, A6, FINSEQ_1:def 7
.= A * j,i by A1, MATRIX_1:def 8
.= (Col A,i) . j by A3, A4, MATRIX_1:def 9 ; :: thesis: verum

end;

hence Col (A ^^ B),i = Col A,i by A2, FINSEQ_2:139; :: thesis: verum