reconsider F1 = <*M1*>, F2 = <*M2*> as FinSequence_of_Square-Matrix of D ;
<*M1,M2*> = F1 ^ F2 ;
hence <*M1,M2*> is FinSequence_of_Square-Matrix of D ; :: thesis: verum