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