let D be non empty set ; :: thesis: for d1, d2, d3 being Element of D holds <*<*d1,d2,d3*>*> is Matrix of 1,3,D
let d1, d2, d3 be Element of D; :: thesis: <*<*d1,d2,d3*>*> is Matrix of 1,3,D
A1: <*d1,d2,d3*> is FinSequence of D by FINSEQ_2:14;
len <*d1,d2,d3*> = 3 by FINSEQ_1:45;
hence <*<*d1,d2,d3*>*> is Matrix of 1,3,D by A1, MATRIX_0:11; :: thesis: verum