set RG = R (+) G;
let i be Nat; :: according to MATRIXJ1:def 6 :: thesis: ( i in dom (R (+) G) implies ex n being Nat st (R (+) G) . i is Matrix of n, the carrier of K )
assume i in dom (R (+) G) ; :: thesis: ex n being Nat st (R (+) G) . i is Matrix of n, the carrier of 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 ; :: thesis: (R (+) G) . i is Matrix of n, the carrier of 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_0:24;
hence (R (+) G) . i is Matrix of n,K by A2, A1, A3, A4, MATRIX_0:24, MATRIX_0:51; :: thesis: verum