:: deftheorem Def2 defines Matrix-yielding MATRIXJ1:def 2 :
for D being non empty set
for F being FinSequence of (D *) * holds
( F is Matrix-yielding iff for i being Nat st i in dom F holds
F . i is Matrix of D );