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: dom (Col (M1 ^ M2),i) = Seg (len (Col (M1 ^ M2),i)) by FINSEQ_1:def 3;
A4: 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 ;

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 A5: j in dom (Col (M1 ^ M2),i) ; :: thesis: (Col (M1 ^ M2),i) . j = ((Col M1,i) ^ (Col M2,i)) . j
then j in Seg (len (M1 ^ M2)) by A3, 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 and
A8: (M1 ^ M2) * j,i = P . i by MATRIX_1:def 6;
A9: j in dom ((Col M1,i) ^ (Col M2,i)) by A4, A3, A5, FINSEQ_1:def 3;

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 A9, FINSEQ_1:38;

suppose A10: 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 A11: 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
A12: P1 = M1 . j and
A13: M1 * j,i = P1 . i by MATRIX_1:def 6;
P = P1 by A7, A11, A12, FINSEQ_1:def 7;
hence (Col (M1 ^ M2),i) . j = M1 * j,i by A6, A8, A13, MATRIX_1:def 9
.= (Col M1,i) . j by A11, MATRIX_1:def 9
.= ((Col M1,i) ^ (Col M2,i)) . j by A10, 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
A14: n in dom (Col M2,i) and
A15: j = (len (Col M1,i)) + n ;
n in Seg (len (Col M2,i)) by A14, FINSEQ_1:def 3;
then n in Seg (len M2) by MATRIX_1:def 9;
then A16: 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
A17: P2 = M2 . n and
A18: M2 * n,i = P2 . i by MATRIX_1:def 6;
len (Col M2,i) = len M2 by MATRIX_1:def 9;
then ( len (Col M1,i) = len M1 & dom (Col M2,i) = dom M2 ) by FINSEQ_3:31, MATRIX_1:def 9;
then P = P2 by A7, A14, A15, A17, FINSEQ_1:def 7;
hence (Col (M1 ^ M2),i) . j = M2 * n,i by A6, A8, A18, MATRIX_1:def 9
.= (Col M2,i) . n by A16, MATRIX_1:def 9
.= ((Col M1,i) ^ (Col M2,i)) . j by A14, A15, 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 A4, FINSEQ_2:10; :: thesis: verum