let D be non empty set ; :: thesis: for p being FinSequence of D holds <*p*> is Matrix of 1, len p,D
let p be FinSequence of D; :: thesis: <*p*> is Matrix of 1, len p,D
reconsider p9 = p as Element of D * by FINSEQ_1:def 11;
<*p9*> is tabular by Th3;
then reconsider M = <*p*> as Matrix of D ;
M is 1, len p -size

proof

thus len M = 1 by FINSEQ_1:39; :: according to MATRIX_0:def 2 :: thesis: for p being FinSequence of D st p in rng M holds
len p = len p
let q be FinSequence of D; :: thesis: ( q in rng M implies len q = len p )
assume q in rng M ; :: thesis: len q = len p
then q in {p} by FINSEQ_1:38;
hence len q = len p by TARSKI:def 1; :: thesis: verum

end;

hence <*p*> is Matrix of 1, len p,D ; :: thesis: verum