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