let K be Ring; for A, B being Matrix of K st len A = len B & width A = width B holds
A + B = B + A
let A, B be Matrix of K; ( len A = len B & width A = width B implies A + B = B + A )
assume that
A1:
len A = len B
and
A2:
width A = width B
; A + B = B + A
A3:
width A = width (A + B)
by Def3;
then A4:
width (A + B) = width (B + A)
by A2, Def3;
A5:
len A = len (A + B)
by Def3;
then
dom A = dom (A + B)
by FINSEQ_3:29;
then A6:
Indices A = Indices (A + B)
by A3;
dom A = dom B
by A1, FINSEQ_3:29;
then A7:
Indices B = [:(dom A),(Seg (width A)):]
by A2;
A8:
now for i, j being Nat st [i,j] in Indices (A + B) holds
(A + B) * (i,j) = (B + A) * (i,j)let i,
j be
Nat;
( [i,j] in Indices (A + B) implies (A + B) * (i,j) = (B + A) * (i,j) )assume A9:
[i,j] in Indices (A + B)
;
(A + B) * (i,j) = (B + A) * (i,j)hence (A + B) * (
i,
j) =
(B * (i,j)) + (A * (i,j))
by A6, Def3
.=
(B + A) * (
i,
j)
by A7, A6, A9, Def3
;
verum end;
len (A + B) = len (B + A)
by A1, A5, Def3;
hence
A + B = B + A
by A4, A8, MATRIX_0:21; verum