let K be Field; :: thesis: for A, B being Matrix of K st width A = width B holds
for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let A, B be Matrix of K; :: thesis: ( width A = width B implies for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
assume A1: width A = width B ; :: thesis: for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let i be Nat; :: thesis: ( 1 <= i & i <= len A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
assume ( 1 <= i & i <= len A ) ; :: thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
then i in dom A by FINSEQ_3:25;
hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A1, MATRIX_4:59; :: thesis: verum