let i, j be Nat; :: thesis: for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & 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: ( len M1 = len M2 & width M1 = width M2 & j in Seg (len M1) implies Line (M1 + M2),j = (Line M1,j) + (Line M2,j) )
assume A1: ( len M1 = len M2 & width M1 = width M2 & j in Seg (len M1) ) ; :: thesis: Line (M1 + M2),j = (Line M1,j) + (Line M2,j)
A2: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by Th6;
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 ;

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 A5: ( 1 <= i & i <= len (Line (M1 + M2),j) ) ; :: thesis: (Line (M1 + M2),j) . i = ((Line M1,j) + (Line M2,j)) . i
then A6: i in Seg (width M1) by A4, FINSEQ_1:3;
A7: i in Seg (width M2) by A1, A4, A5, FINSEQ_1:3;
i in Seg (len ((Line M1,j) + (Line M2,j))) by A3, A4, A5, FINSEQ_1:3;
then A8: i in dom ((Line M1,j) + (Line M2,j)) by FINSEQ_1:def 3;
( j in Seg (len M1) & i in Seg (width M1) ) by A1, A4, A5, FINSEQ_1:3;
then [j,i] in [:(Seg (len M1)),(Seg (width M1)):] by ZFMISC_1:106;
then A9: [j,i] in Indices M1 by FINSEQ_1:def 3;
i in Seg (width (M1 + M2)) by A2, A4, A5, 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 A1, A9, Th7
.= (M1 * j,i) + ((Line M2,j) . i) by A7, MATRIX_1:def 8
.= ((Line M1,j) . i) + ((Line M2,j) . i) by A6, MATRIX_1:def 8
.= ((Line M1,j) + (Line M2,j)) . i by A8, COMPLSP2:1 ;
:: thesis: verum

end;

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