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