let D be non empty set ; :: thesis: for a1, a2, a3, b1, b2, b3, c1, c2, c3 being Element of D holds <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D
let a1, a2, a3, b1, b2, b3, c1, c2, c3 be Element of D; :: thesis: <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D
A1: len <*c1,c2,c3*> = 3 by FINSEQ_1:45;
( len <*a1,a2,a3*> = 3 & len <*b1,b2,b3*> = 3 ) by FINSEQ_1:45;
hence <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D by A1, Th34; :: thesis: verum