let K be Ring; 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; ( 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
; M1 - M3 = M4 - M2
A8:
( len (- M2) = len M1 & width (- M2) = width M1 )
by A1, A4, MATRIX_3:def 2;
M1 + M2 = M4 + M3
by A3, A6, A7, MATRIX_3:2;
then
(M1 + M2) + (- M2) = M4 + (M3 + (- M2))
by A3, A6, MATRIX_3:3;
then
(M1 + M2) + (- M2) = M4 + ((- M2) + M3)
by A1, A2, A4, A5, A8, MATRIX_3:2;
then
M1 + (M2 - M2) = M4 + ((- M2) + M3)
by A1, A4, MATRIX_3:3;
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 A1, A2, A3, A4, A5, A6, MATRIX_3:def 3;
hence
M1 - M3 = M4 - M2
by A1, A2, A4, A5, A9, Th21; verum