let k, m, n 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 ^^ B) = n by MATRIX_0:def 2;
A3: len A = n by MATRIX_0:def 2;

now :: thesis: for j being Nat st j in Seg n holds
(Col ((A ^^ B),i)) . j = (Col (A,i)) . j

let j be Nat; :: thesis: ( j in Seg n implies (Col ((A ^^ B),i)) . j = (Col (A,i)) . j )
assume A4: j in Seg n ; :: thesis: (Col ((A ^^ B),i)) . j = (Col (A,i)) . j
n <> 0 by A4;
then width (A ^^ B) = (width A) + (width B) by MATRIX_0:23;
then width A <= width (A ^^ B) by NAT_1:11;
then A5: Seg (width A) c= Seg (width (A ^^ B)) by FINSEQ_1:5;
A6: dom A = Seg n by A3, FINSEQ_1:def 3;
A7: dom (Line (A,j)) = Seg (width A) by FINSEQ_2:124;
dom (A ^^ B) = Seg n by A2, FINSEQ_1:def 3;
hence (Col ((A ^^ B),i)) . j = (A ^^ B) * (j,i) by A4, MATRIX_0:def 8
.= (Line ((A ^^ B),j)) . i by A1, A5, MATRIX_0:def 7
.= ((Line (A,j)) ^ (Line (B,j))) . i by A4, Th15
.= (Line (A,j)) . i by A1, A7, FINSEQ_1:def 7
.= A * (j,i) by A1, MATRIX_0:def 7
.= (Col (A,i)) . j by A4, A6, MATRIX_0:def 8 ;
:: thesis: verum

end;

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