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