:: deftheorem Def6 defines Square-Matrix-yielding MATRIXJ1:def 6 :
for D being non empty set
for F being FinSequence of (D *) * holds
( F is Square-Matrix-yielding iff for i being Nat st i in dom F holds
ex n being Nat st F . i is Matrix of n,D );