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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
hence (Col ((M1 ^ M2),i)) . j = M1 * (j,i) by
.= (Col (M1,i)) . j by
.= ((Col (M1,i)) ^ (Col (M2,i))) . j by ;
:: 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 ;
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 ;
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 ;
then P = P2 by ;
hence (Col ((M1 ^ M2),i)) . j = M2 * (n,i) by
.= (Col (M2,i)) . n by
.= ((Col (M1,i)) ^ (Col (M2,i))) . j by ;
:: 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 ; :: thesis: verum