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