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_0:def 7
.= len (Line (M1,j)) by MATRIX_0:def 7 ;
then A3: len ((Line (M1,j)) + (Line (M2,j))) = len (Line (M1,j)) by COMPLSP2:6
.= width M1 by MATRIX_0:def 7 ;
A4: len (Line ((M1 + M2),j)) = width (M1 + M2) by MATRIX_0:def 7
.= width M1 by Th5 ;
A5: width (M1 + M2) = width M1 by Th5;

now :: thesis: for i being Nat st 1 <= i & i <= len (Line ((M1 + M2),j)) holds
(Line ((M1 + M2),j)) . i = ((Line (M1,j)) + (Line (M2,j))) . i

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:1;
i in Seg (width M1) by A4, A6, A7, FINSEQ_1:1;
then [j,i] in [:(Seg (len M1)),(Seg (width M1)):] by A2, ZFMISC_1:87;
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:1;
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:1;
i in Seg (width (M1 + M2)) by A5, A4, A6, A7, FINSEQ_1:1;
hence (Line ((M1 + M2),j)) . i = (M1 + M2) * (j,i) by MATRIX_0:def 7
.= (M1 * (j,i)) + (M2 * (j,i)) by A9, Th6
.= (M1 * (j,i)) + ((Line (M2,j)) . i) by A11, MATRIX_0:def 7
.= ((Line (M1,j)) . i) + ((Line (M2,j)) . i) by A8, MATRIX_0:def 7
.= ((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:14; :: thesis: verum