let i, j be Nat; :: thesis: for M1, M2 being Matrix of COMPLEX st width M1 = width M2 & j in Seg (len M1) holds
Line (M1 + M2),j = (Line M1,j) + (Line M2,j)
let M1, M2 be Matrix of COMPLEX ; :: thesis: ( width M1 = width M2 & j in Seg (len M1) implies Line (M1 + M2),j = (Line M1,j) + (Line M2,j) )
assume that
A1: width M1 = width M2 and
A2: j in Seg (len M1) ; :: thesis: Line (M1 + M2),j = (Line M1,j) + (Line M2,j)
len (Line M2,j) = width M1 by A1, MATRIX_1:def 8
.= len (Line M1,j) by MATRIX_1:def 8 ;
then A3: len ((Line M1,j) + (Line M2,j)) = len (Line M1,j) by COMPLSP2:6
.= width M1 by MATRIX_1:def 8 ;
A4: len (Line (M1 + M2),j) = width (M1 + M2) by MATRIX_1:def 8
.= width M1 by Th6 ;
A5: width (M1 + M2) = width M1 by Th6;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len (Line (M1 + M2),j) implies (Line (M1 + M2),j) . i = ((Line M1,j) + (Line M2,j)) . i )
assume that
A6: 1 <= i and
A7: i <= len (Line (M1 + M2),j) ; :: thesis: (Line (M1 + M2),j) . i = ((Line M1,j) + (Line M2,j)) . i
A8: i in Seg (width M1) by A4, A6, A7, FINSEQ_1:3;
i in Seg (width M1) by A4, A6, A7, FINSEQ_1:3;
then [j,i] in [:(Seg (len M1)),(Seg (width M1)):] by A2, ZFMISC_1:106;
then A9: [j,i] in Indices M1 by FINSEQ_1:def 3;
i in Seg (len ((Line M1,j) + (Line M2,j))) by A3, A4, A6, A7, FINSEQ_1:3;
then A10: i in dom ((Line M1,j) + (Line M2,j)) by FINSEQ_1:def 3;
A11: i in Seg (width M2) by A1, A4, A6, A7, FINSEQ_1:3;
i in Seg (width (M1 + M2)) by A5, A4, A6, A7, FINSEQ_1:3;
hence (Line (M1 + M2),j) . i = (M1 + M2) * j,i by MATRIX_1:def 8
.= (M1 * j,i) + (M2 * j,i) by A9, Th7
.= (M1 * j,i) + ((Line M2,j) . i) by A11, MATRIX_1:def 8
.= ((Line M1,j) . i) + ((Line M2,j) . i) by A8, MATRIX_1:def 8
.= ((Line M1,j) + (Line M2,j)) . i by A10, COMPLSP2:1 ;
:: thesis: verum

end;

hence Line (M1 + M2),j = (Line M1,j) + (Line M2,j) by A3, A4, FINSEQ_1:18; :: thesis: verum