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,K )
assume i in dom (mlt p,R) ; :: thesis: ex n being Nat st (mlt p,R) . i is Matrix of n,K
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,K ;
take n = n; :: thesis: (mlt p,R) . i is Matrix of n,K
len (R . i) = n by A2, MATRIX_1:25;
hence (mlt p,R) . i is Matrix of n,K by A1; :: thesis: verum

end;

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