let F be FinSequence of (D * ) * ; :: thesis: ( F is Square-Matrix-yielding implies F is Matrix-yielding )
assume A1: F is Square-Matrix-yielding ; :: thesis: F is Matrix-yielding
let i be Nat; :: according to MATRIXJ1:def 2 :: thesis: ( i in dom F implies F . i is Matrix of D )
assume A2: i in dom F ; :: thesis: F . i is Matrix of D
ex n being Nat st F . i is Matrix of n,D by A1, A2, Def6;
hence F . i is Matrix of D ; :: thesis: verum