let n be Nat; :: thesis: for K being Field
for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
let K be Field; :: thesis: for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
let a9, b9 be Element of K; :: thesis: ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
A1: Indices ((n,n) --> a9) = Indices ((n,n) --> (a9 + b9)) by MATRIX_1:26;
A2: Indices ((n,n) --> a9) = Indices ((n,n) --> b9) by MATRIX_1:26;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices ((n,n) --> (a9 + b9)) implies (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j) )
assume A3: [i,j] in Indices ((n,n) --> (a9 + b9)) ; :: thesis: (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j)
then ((n,n) --> a9) * (i,j) = a9 by A1, Th1;
then (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = a9 + b9 by A2, A1, A3, Th1;
hence (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j) by A3, Th1; :: thesis: verum

end;

hence ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9) by A1, MATRIX_1:def 13; :: thesis: verum