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 i in dom F ; :: thesis: F . i is Matrix of D
then ex n being Nat st F . i is Matrix of n,D by A1;
hence F . i is Matrix of D ; :: thesis: verum