let D be non empty set ; :: thesis: for a1, a2 being Element of D holds <*<*a1,a2*>*> is Matrix of 1,2,D
let a1, a2 be Element of D; :: thesis: <*<*a1,a2*>*> is Matrix of 1,2,D
( <*a1,a2*> is FinSequence of D & len <*a1,a2*> = 2 ) by FINSEQ_1:61, FINSEQ_2:15;
hence <*<*a1,a2*>*> is Matrix of 1,2,D by Th11; :: thesis: verum