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 A1: i in dom (R (+) G) ; :: thesis: ex n being Nat st (R (+) G) . i is Matrix of n,K
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
( len (R . i) = n & width (R . i) = n & (R (+) G) . i = (R . i) + (G . i) & len ((R . i) + (G . i)) = len (R . i) & width ((R . i) + (G . i)) = width (R . i) ) by A1, A2, Def10, MATRIX_1:25, MATRIX_3:def 3;
hence (R (+) G) . i is Matrix of n,K by MATRIX_2:7; :: thesis: verum

end;

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