let n, k, m be Nat; :: thesis: for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
for i being Nat st i in Seg (width M1) holds
Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i)
let D be non empty set ; :: thesis: for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
for i being Nat st i in Seg (width M1) holds
Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i)
let M1 be Matrix of n,k,D; :: thesis: for M2 being Matrix of m,k,D st width M1 = width M2 holds
for i being Nat st i in Seg (width M1) holds
Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i)
let M2 be Matrix of m,k,D; :: thesis: ( width M1 = width M2 implies for i being Nat st i in Seg (width M1) holds
Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i) )
assume A1: width M1 = width M2 ; :: thesis: for i being Nat st i in Seg (width M1) holds
Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i)
let i be Nat; :: thesis: ( i in Seg (width M1) implies Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i) )
assume A2: i in Seg (width M1) ; :: thesis: Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i)
A3: len (Col (M1 ^ M2),i) = len (M1 ^ M2) by MATRIX_1:def 9
.= (len M1) + (len M2) by FINSEQ_1:35
.= (len M1) + (len (Col M2,i)) by MATRIX_1:def 9
.= (len (Col M1,i)) + (len (Col M2,i)) by MATRIX_1:def 9
.= len ((Col M1,i) ^ (Col M2,i)) by FINSEQ_1:35 ;
X: dom (Col (M1 ^ M2),i) = Seg (len (Col (M1 ^ M2),i)) by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom (Col (M1 ^ M2),i) implies (Col (M1 ^ M2),i) . j = ((Col M1,i) ^ (Col M2,i)) . j )
assume A4: j in dom (Col (M1 ^ M2),i) ; :: thesis: (Col (M1 ^ M2),i) . j = ((Col M1,i) ^ (Col M2,i)) . j
then A5: j in dom ((Col M1,i) ^ (Col M2,i)) by X, A3, FINSEQ_1:def 3;
j in Seg (len (M1 ^ M2)) by A4, X, MATRIX_1:def 9;
then A6: j in dom (M1 ^ M2) by FINSEQ_1:def 3;
i in Seg (width (M1 ^ M2)) by A1, A2, Th28;
then [j,i] in [:(dom (M1 ^ M2)),(Seg (width (M1 ^ M2))):] by A6, ZFMISC_1:106;
then [j,i] in Indices (M1 ^ M2) by MATRIX_1:def 5;
then consider P being FinSequence of D such that
A7: ( P = (M1 ^ M2) . j & (M1 ^ M2) * j,i = P . i ) by MATRIX_1:def 6;

now

per cases ( j in dom (Col M1,i) or ex n being Nat st
( n in dom (Col M2,i) & j = (len (Col M1,i)) + n ) ) by A5, FINSEQ_1:38;

suppose A8: j in dom (Col M1,i) ; :: thesis: (Col (M1 ^ M2),i) . j = ((Col M1,i) ^ (Col M2,i)) . j

then j in Seg (len (Col M1,i)) by FINSEQ_1:def 3;
then j in Seg (len M1) by MATRIX_1:def 9;
then A9: j in dom M1 by FINSEQ_1:def 3;
then [j,i] in [:(dom M1),(Seg (width M1)):] by A2, ZFMISC_1:106;
then [j,i] in Indices M1 by MATRIX_1:def 5;
then consider P1 being FinSequence of D such that
A10: ( P1 = M1 . j & M1 * j,i = P1 . i ) by MATRIX_1:def 6;
P = P1 by A7, A9, A10, FINSEQ_1:def 7;
hence (Col (M1 ^ M2),i) . j = M1 * j,i by A6, A7, A10, MATRIX_1:def 9
.= (Col M1,i) . j by A9, MATRIX_1:def 9
.= ((Col M1,i) ^ (Col M2,i)) . j by A8, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom (Col M2,i) & j = (len (Col M1,i)) + n ) ; :: thesis: (Col (M1 ^ M2),i) . j = ((Col M1,i) ^ (Col M2,i)) . j

then consider n being Nat such that
A11: ( n in dom (Col M2,i) & j = (len (Col M1,i)) + n ) ;
n in Seg (len (Col M2,i)) by A11, FINSEQ_1:def 3;
then n in Seg (len M2) by MATRIX_1:def 9;
then A12: n in dom M2 by FINSEQ_1:def 3;
then [n,i] in [:(dom M2),(Seg (width M2)):] by A1, A2, ZFMISC_1:106;
then [n,i] in Indices M2 by MATRIX_1:def 5;
then consider P2 being FinSequence of D such that
A13: ( P2 = M2 . n & M2 * n,i = P2 . i ) by MATRIX_1:def 6;
A14: len (Col M1,i) = len M1 by MATRIX_1:def 9;
len (Col M2,i) = len M2 by MATRIX_1:def 9;
then dom (Col M2,i) = dom M2 by FINSEQ_3:31;
then P = P2 by A7, A11, A13, A14, FINSEQ_1:def 7;
hence (Col (M1 ^ M2),i) . j = M2 * n,i by A6, A7, A13, MATRIX_1:def 9
.= (Col M2,i) . n by A12, MATRIX_1:def 9
.= ((Col M1,i) ^ (Col M2,i)) . j by A11, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence (Col (M1 ^ M2),i) . j = ((Col M1,i) ^ (Col M2,i)) . j ; :: thesis: verum

end;

hence Col (M1 ^ M2),i = (Col M1,i) ^ (Col M2,i) by A3, FINSEQ_2:10; :: thesis: verum