set RG = R (+) G;

now

let i be Nat; :: thesis: ( i in dom (R (+) G) implies ex n being Nat st (R (+) G) . i is Matrix of n,K )
assume i in dom (R (+) G) ; :: thesis: ex n being Nat st (R (+) G) . i is Matrix of n,K
then A1: (R (+) G) . i = (R . i) + (G . i) by Def10;
consider n being Nat such that
A2: R . i is Matrix of n,K ;
take n = n; :: thesis: (R (+) G) . i is Matrix of n,K
A3: len ((R . i) + (G . i)) = len (R . i) by MATRIX_3:def 3;
A4: width ((R . i) + (G . i)) = width (R . i) by MATRIX_3:def 3;
width (R . i) = n by A2, MATRIX_1:25;
hence (R (+) G) . i is Matrix of n,K by A2, A1, A3, A4, MATRIX_1:25, MATRIX_2:7; :: thesis: verum

end;

hence R (+) G is FinSequence_of_Square-Matrix of K by Def6; :: thesis: verum