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

now :: thesis: for i, j being Nat st [i,j] in Indices ((n,n) --> (a + b)) holds
(((n,n) --> a) * (i,j)) + (((n,n) --> b) * (i,j)) = ((n,n) --> (a + b)) * (i,j)

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

end;

hence ((n,n) --> a) + ((n,n) --> b) = (n,n) --> (a + b) by A1, Def5; :: thesis: verum