let D be non empty set ; :: thesis: for M being Matrix of D holds Width <*M*> = <*(width M)*>
let M be Matrix of D; :: thesis: Width <*M*> = <*(width M)*>
set F = <*M*>;
A1: len <*M*> = 1 by FINSEQ_1:57;
A2: <*M*> . 1 = M by FINSEQ_1:57;
A3: len <*M*> = len (Width <*M*>) by FINSEQ_1:def 18;
A4: dom (Width <*M*>) = Seg (len <*M*>) by FINSEQ_2:144;
1 in Seg 1 ;
then (Width <*M*>) . 1 = width (<*M*> . 1) by A1, A4, Def4;
hence Width <*M*> = <*(width M)*> by A1, A3, A2, FINSEQ_1:57; :: thesis: verum