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