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

end;

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