let k, n, m, l be Nat; :: thesis: for A being Matrix of n,k,REAL
for B being Matrix of k,m,REAL
for C being Matrix of m,l,REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)
let A be Matrix of n,k,REAL; :: thesis: for B being Matrix of k,m,REAL
for C being Matrix of m,l,REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)
let B be Matrix of k,m,REAL; :: thesis: for C being Matrix of m,l,REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)
let C be Matrix of m,l,REAL; :: thesis: ( n > 0 & k > 0 & m > 0 implies (A * B) * C = A * (B * C) )
assume that
A1: n > 0 and
A2: k > 0 and
A3: m > 0 ; :: thesis: (A * B) * C = A * (B * C)
A4: ( width B = m & len C = m ) by A2, A3, MATRIX_0:23;
( width A = k & len B = k ) by A1, A2, MATRIX_0:23;
hence (A * B) * C = A * (B * C) by A4, MATRIX_3:33; :: thesis: verum