let D be non empty set ; 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; <*<*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; verum