let D be non empty set ; :: thesis: {} is FinSequence_of_Matrix of D
set F = <*> ((D *) *);
for i being Nat st i in dom (<*> ((D *) *)) holds
(<*> ((D *) *)) . i is Matrix of D ;
hence {} is FinSequence_of_Matrix of D by Def2; :: thesis: verum