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