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 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 (A ^^ B) = n by MATRIX_0:def 2;

A3: len B = n by MATRIX_0:def 2;

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 (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),((width A) + i))) . j = (Col (B,i)) . j

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

A4:
dom B = Seg n
by A3, FINSEQ_1:def 3;

let j be Nat; :: thesis: ( j in Seg n implies (Col ((A ^^ B),((width A) + i))) . j = (Col (B,i)) . j )

assume A5: j in Seg n ; :: thesis: (Col ((A ^^ B),((width A) + i))) . j = (Col (B,i)) . j

n <> 0 by A5;

then width (A ^^ B) = (width A) + (width B) by MATRIX_0:23;

then A6: (width A) + i in Seg (width (A ^^ B)) by A1, FINSEQ_1:60;

A7: ( dom (Line (B,j)) = Seg (width B) & len (Line (A,j)) = width A ) by CARD_1:def 7, FINSEQ_2:124;

dom (A ^^ B) = Seg n by A2, FINSEQ_1:def 3;

hence (Col ((A ^^ B),((width A) + i))) . j = (A ^^ B) * (j,((width A) + i)) by A5, MATRIX_0:def 8

.= (Line ((A ^^ B),j)) . ((width A) + i) by A6, MATRIX_0:def 7

.= ((Line (A,j)) ^ (Line (B,j))) . ((width A) + i) by A5, Th15

.= (Line (B,j)) . i by A1, A7, FINSEQ_1:def 7

.= B * (j,i) by A1, MATRIX_0:def 7

.= (Col (B,i)) . j by A5, A4, MATRIX_0:def 8 ;

:: thesis: verum

end;let j be Nat; :: thesis: ( j in Seg n implies (Col ((A ^^ B),((width A) + i))) . j = (Col (B,i)) . j )

assume A5: j in Seg n ; :: thesis: (Col ((A ^^ B),((width A) + i))) . j = (Col (B,i)) . j

n <> 0 by A5;

then width (A ^^ B) = (width A) + (width B) by MATRIX_0:23;

then A6: (width A) + i in Seg (width (A ^^ B)) by A1, FINSEQ_1:60;

A7: ( dom (Line (B,j)) = Seg (width B) & len (Line (A,j)) = width A ) by CARD_1:def 7, FINSEQ_2:124;

dom (A ^^ B) = Seg n by A2, FINSEQ_1:def 3;

hence (Col ((A ^^ B),((width A) + i))) . j = (A ^^ B) * (j,((width A) + i)) by A5, MATRIX_0:def 8

.= (Line ((A ^^ B),j)) . ((width A) + i) by A6, MATRIX_0:def 7

.= ((Line (A,j)) ^ (Line (B,j))) . ((width A) + i) by A5, Th15

.= (Line (B,j)) . i by A1, A7, FINSEQ_1:def 7

.= B * (j,i) by A1, MATRIX_0:def 7

.= (Col (B,i)) . j by A5, A4, MATRIX_0:def 8 ;

:: thesis: verum