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

now

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, Th1;
then ((n,n --> a') * i,j) + ((n,n --> b') * i,j) = a' + b' by A2, A1, A3, Th1;
hence ((n,n --> a') * i,j) + ((n,n --> b') * i,j) = (n,n --> (a' + b')) * i,j by A3, Th1; :: thesis: verum

end;

hence (n,n --> a') + (n,n --> b') = n,n --> (a' + b') by A1, MATRIX_1:def 14; :: thesis: verum