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