let m, n be Nat; :: thesis: for M being Matrix of m,F_Real
for N being Matrix of m,n,F_Real st m > 0 holds
M * N is Matrix of m,n,F_Real
let M be Matrix of m,F_Real; :: thesis: for N being Matrix of m,n,F_Real st m > 0 holds
M * N is Matrix of m,n,F_Real
let N be Matrix of m,n,F_Real; :: thesis: ( m > 0 implies M * N is Matrix of m,n,F_Real )
assume A1: m > 0 ; :: thesis: M * N is Matrix of m,n,F_Real
( len N = m & width N = n ) by A1, MATRIX_0:23;
then width M = len N by A1, MATRIX_0:23;
then ( len (M * N) = len M & width (M * N) = width N ) by MATRIX_3:def 4;
then ( len (M * N) = m & width (M * N) = n ) by A1, MATRIX_0:23;
hence M * N is Matrix of m,n,F_Real by A1, MATRIX_0:20; :: thesis: verum