let D be non empty set ; :: thesis: <*{} ,{} *> is Matrix of 2, 0 ,D
len (<*> D) = 0 ;
hence <*{} ,{} *> is Matrix of 2, 0 ,D by Th12; :: thesis: verum