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