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