let n, k, m, l be Element of 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_1:24;
( width A = k & len B = k ) by A1, A2, MATRIX_1:24;
hence (A * B) * C = A * (B * C) by A4, MATRIX_3:35; :: thesis: verum