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 () holds
Col ((A ^^ B),(() + 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 () holds
Col ((A ^^ B),(() + 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 () holds
Col ((A ^^ B),(() + i)) = Col (B,i)

let B be Matrix of n,k,D; :: thesis: for i being Nat st i in Seg () holds
Col ((A ^^ B),(() + i)) = Col (B,i)

let i be Nat; :: thesis: ( i in Seg () implies Col ((A ^^ B),(() + i)) = Col (B,i) )
assume A1: i in Seg () ; :: thesis: Col ((A ^^ B),(() + i)) = Col (B,i)
set AB = A ^^ B;
A2: len (A ^^ B) = n by MATRIX_0:def 2;
A3: len B = n by MATRIX_0:def 2;
now :: thesis: for j being Nat st j in Seg n holds
(Col ((A ^^ B),(() + i))) . j = (Col (B,i)) . j
A4: dom B = Seg n by ;
let j be Nat; :: thesis: ( j in Seg n implies (Col ((A ^^ B),(() + i))) . j = (Col (B,i)) . j )
assume A5: j in Seg n ; :: thesis: (Col ((A ^^ B),(() + i))) . j = (Col (B,i)) . j
n <> 0 by A5;
then width (A ^^ B) = () + () by MATRIX_0:23;
then A6: (width A) + i in Seg (width (A ^^ B)) by ;
A7: ( dom (Line (B,j)) = Seg () & len (Line (A,j)) = width A ) by ;
dom (A ^^ B) = Seg n by ;
hence (Col ((A ^^ B),(() + i))) . j = (A ^^ B) * (j,(() + i)) by
.= (Line ((A ^^ B),j)) . (() + i) by
.= ((Line (A,j)) ^ (Line (B,j))) . (() + i) by
.= (Line (B,j)) . i by
.= B * (j,i) by
.= (Col (B,i)) . j by ;
:: thesis: verum
end;
hence Col ((A ^^ B),(() + i)) = Col (B,i) by ; :: thesis: verum