let K be Ring; :: thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds
(B - C) * A = (B * A) - (C * A)
let A, B, C be Matrix of K; :: thesis: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 implies (B - C) * A = (B * A) - (C * A) )
assume A1: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 ) ; :: thesis: (B - C) * A = (B * A) - (C * A)
A2: ( width (- C) = width C & len C = len (- C) ) by MATRIX_3:def 2;
thus (B - C) * A = (B + (- C)) * A by MATRIX_4:def 1
.= (B * A) + ((- C) * A) by A1, A2, MATRIX_4:63
.= (B * A) + (- (C * A)) by A1, Th15
.= (B * A) - (C * A) by MATRIX_4:def 1 ; :: thesis: verum