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