let n be Nat; :: thesis: for D being non empty set
for M being Matrix of n,D holds <*M*> is FinSequence_of_Square-Matrix of D
let D be non empty set ; :: thesis: for M being Matrix of n,D holds <*M*> is FinSequence_of_Square-Matrix of D
let M be Matrix of n,D; :: 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,D )
assume A1: i in dom <*M*> ; :: thesis: ex n being Nat st <*M*> . i is Matrix of n,D
take n = n; :: thesis: <*M*> . i is Matrix of n,D
dom <*M*> = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then ( <*M*> . 1 = M & i = 1 ) by A1, FINSEQ_1:def 8, TARSKI:def 1;
hence <*M*> . i is Matrix of n,D ; :: thesis: verum

end;

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