set M = mlt p,R;
let i be Nat; :: according to MATRIXJ1:def 6 :: thesis: ( i in dom (mlt p,R) implies ex n being Nat st (mlt p,R) . i is Matrix of n,the carrier of K )
assume i in dom (mlt p,R) ; :: thesis: ex n being Nat st (mlt p,R) . i is Matrix of n,the carrier of 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 ; :: thesis: (mlt p,R) . i is Matrix of n,the carrier of K
len (R . i) = n by A2, MATRIX_1:25;
hence (mlt p,R) . i is Matrix of n,K by A1; :: thesis: verum