let D be non empty set ; :: thesis: for d1, d2, d3 being Element of D holds <*<*d1*>,<*d2*>,<*d3*>*> is Matrix of 3,1,D
let d1, d2, d3 be Element of D; :: thesis: <*<*d1*>,<*d2*>,<*d3*>*> is Matrix of 3,1,D
reconsider p = <*d1*>, q = <*d2*>, r = <*d3*> as FinSequence of D ;
( len p = 1 & len q = 1 & len r = 1 ) by FINSEQ_1:40;
hence <*<*d1*>,<*d2*>,<*d3*>*> is Matrix of 3,1,D by MATRIXR2:34; :: thesis: verum