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 :: thesis: for i being Nat st i in dom <*M*> holds
ex n being Nat st <*M*> . i is Matrix of n,D
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
A2: <*M*> . 1 = M by FINSEQ_1:def 8;
dom <*M*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
hence <*M*> . i is Matrix of n,D by A1, A2, TARSKI:def 1; :: thesis: verum
end;
hence <*M*> is FinSequence_of_Square-Matrix of D by Def6; :: thesis: verum