let K be Field; :: thesis: for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 + M4 holds
M1 - M3 = M4 - M2

let M1, M2, M3, M4 be Matrix of K; :: thesis: ( len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 + M4 implies M1 - M3 = M4 - M2 )
assume that
A1: len M1 = len M2 and
A2: len M2 = len M3 and
A3: len M3 = len M4 and
A4: width M1 = width M2 and
A5: width M2 = width M3 and
A6: width M3 = width M4 and
A7: M1 + M2 = M3 + M4 ; :: thesis: M1 - M3 = M4 - M2
A8: ( len (- M2) = len M1 & width (- M2) = width M1 ) by ;
M1 + M2 = M4 + M3 by ;
then (M1 + M2) + (- M2) = M4 + (M3 + (- M2)) by ;
then (M1 + M2) + (- M2) = M4 + ((- M2) + M3) by A1, A2, A4, A5, A8, MATRIX_3:2;
then M1 + (M2 - M2) = M4 + ((- M2) + M3) by ;
then M1 = M4 + ((- M2) + M3) by A1, A4, Th20;
then A9: M1 = (M4 + (- M2)) + M3 by A1, A2, A3, A4, A5, A6, A8, MATRIX_3:3;
( len (M4 + (- M2)) = len M1 & width (M4 + (- M2)) = width M1 ) by ;
hence M1 - M3 = M4 - M2 by A1, A2, A4, A5, A9, Th21; :: thesis: verum