let k, m, n 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_0:def 8
.= (len M1) + (len M2) by FINSEQ_1:22
.= (len M1) + (len (Col (M2,i))) by MATRIX_0:def 8
.= (len (Col (M1,i))) + (len (Col (M2,i))) by MATRIX_0:def 8
.= len ((Col (M1,i)) ^ (Col (M2,i))) by FINSEQ_1:22 ;

now :: thesis: for j being Nat st j in dom (Col ((M1 ^ M2),i)) holds
(Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j

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_0:def 8;
then A6: j in dom (M1 ^ M2) by FINSEQ_1:def 3;
i in Seg (width (M1 ^ M2)) by A1, A2, Th24;
then [j,i] in [:(dom (M1 ^ M2)),(Seg (width (M1 ^ M2))):] by A6, ZFMISC_1:87;
then [j,i] in Indices (M1 ^ M2) by MATRIX_0:def 4;
then consider P being FinSequence of D such that
A7: P = (M1 ^ M2) . j and
A8: (M1 ^ M2) * (j,i) = P . i by MATRIX_0:def 5;
A9: j in dom ((Col (M1,i)) ^ (Col (M2,i))) by A4, A3, A5, FINSEQ_1:def 3;

now :: thesis: (Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j

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:25;

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_0:def 8;
then A11: j in dom M1 by FINSEQ_1:def 3;
then [j,i] in [:(dom M1),(Seg (width M1)):] by A2, ZFMISC_1:87;
then [j,i] in Indices M1 by MATRIX_0:def 4;
then consider P1 being FinSequence of D such that
A12: P1 = M1 . j and
A13: M1 * (j,i) = P1 . i by MATRIX_0:def 5;
P = P1 by A7, A11, A12, FINSEQ_1:def 7;
hence (Col ((M1 ^ M2),i)) . j = M1 * (j,i) by A6, A8, A13, MATRIX_0:def 8
.= (Col (M1,i)) . j by A11, MATRIX_0:def 8
.= ((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_0:def 8;
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:87;
then [n,i] in Indices M2 by MATRIX_0:def 4;
then consider P2 being FinSequence of D such that
A17: P2 = M2 . n and
A18: M2 * (n,i) = P2 . i by MATRIX_0:def 5;
len (Col (M2,i)) = len M2 by MATRIX_0:def 8;
then ( len (Col (M1,i)) = len M1 & dom (Col (M2,i)) = dom M2 ) by FINSEQ_3:29, MATRIX_0:def 8;
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_0:def 8
.= (Col (M2,i)) . n by A16, MATRIX_0:def 8
.= ((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:9; :: thesis: verum