let D be non empty set ; :: thesis: for M being Matrix of D holds len (Mx2FinS M) = (len M) * (width M)
let M be Matrix of D; :: thesis: len (Mx2FinS M) = (len M) * (width M)

per cases ( len M = 0 or len M > 0 ) ;

suppose A1: len M = 0 ; :: thesis: len (Mx2FinS M) = (len M) * (width M)

then Mx2FinS M = {} by Def5;
hence len (Mx2FinS M) = (len M) * (width M) by A1; :: thesis: verum

end;

suppose A2: len M > 0 ; :: thesis: len (Mx2FinS M) = (len M) * (width M)

then consider p being FinSequence of D * such that
A3: Mx2FinS M = p . (len M) and
A4: len p = len M and
A5: p . 1 = M . 1 and
A6: for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) by Def5;
len M in Seg (len M) by A2, FINSEQ_1:3;
then len M in dom p by A4, FINSEQ_1:def 3;
hence len (Mx2FinS M) = (len M) * (width M) by A3, A4, A5, A6, Th29; :: thesis: verum

end;

end;