set M = mlt p,R;

now

let i be Nat; :: thesis: ( i in dom (mlt p,R) implies ex n being Nat st (mlt p,R) . i is Matrix of n, )
assume i in dom (mlt p,R) ; :: thesis: ex n being Nat st (mlt p,R) . i is Matrix of n,
then A1: (mlt p,R) . i = (p /. i) * (R . i) by Def9;
consider n being Nat such that
A2: R . i is Matrix of n, ;
take n = n; :: thesis: (mlt p,R) . i is Matrix of n,
len (R . i) = n by A2, MATRIX_1:25;
hence (mlt p,R) . i is Matrix of n, by A1; :: thesis: verum

end;

hence mlt p,R is FinSequence_of_Square-Matrix of K by Def6; :: thesis: verum