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 ;

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

hence
Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))
by A4, FINSEQ_2:9; :: thesis: verum(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;

end;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))) . jend;

hence
(Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j
; :: thesis: verumper 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;

end;

( 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;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

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

( 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;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