let n be Nat; :: thesis: for D being non empty set
for M being Matrix of n, holds <*M*> is FinSequence_of_Square-Matrix of D
let D be non empty set ; :: thesis: for M being Matrix of n, holds <*M*> is FinSequence_of_Square-Matrix of D
let M be Matrix of n, ; :: thesis: <*M*> is FinSequence_of_Square-Matrix of D

now

let i be Nat; :: thesis: ( i in dom <*M*> implies ex n being Nat st <*M*> . i is Matrix of n, )
assume A1: i in dom <*M*> ; :: thesis: ex n being Nat st <*M*> . i is Matrix of n,
take n = n; :: thesis: <*M*> . i is Matrix of n,
A2: <*M*> . 1 = M by FINSEQ_1:def 8;
dom <*M*> = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
hence <*M*> . i is Matrix of n, by A1, A2, TARSKI:def 1; :: thesis: verum

end;

hence <*M*> is FinSequence_of_Square-Matrix of D by Def6; :: thesis: verum