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_0:24;
hence (mlt (p,R)) . i is Matrix of n,K by A1; :: thesis: verum