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