reconsider F1 = <*M1*>, F2 = <*M2*> as FinSequence_of_Matrix of D by Lm3;
<*M1,M2*> = F1 ^ F2 ;
hence <*M1,M2*> is FinSequence_of_Matrix of D ; :: thesis: verum