let n be Nat; for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)
let A, B, C be Matrix of n,F; (A + B) + C = A + (B + C)
A1:
Indices A = Indices ((A + B) + C)
by MATRIX_0:26;
A2:
Indices A = Indices (A + B)
by MATRIX_0:26;
A3:
Indices A = Indices B
by MATRIX_0:26;
now for i, j being Nat st [i,j] in Indices ((A + B) + C) holds
((A + B) + C) * (i,j) = (A + (B + C)) * (i,j)let i,
j be
Nat;
( [i,j] in Indices ((A + B) + C) implies ((A + B) + C) * (i,j) = (A + (B + C)) * (i,j) )assume A4:
[i,j] in Indices ((A + B) + C)
;
((A + B) + C) * (i,j) = (A + (B + C)) * (i,j)hence ((A + B) + C) * (
i,
j) =
((A + B) * (i,j)) + (C * (i,j))
by A1, A2, Def5
.=
((A * (i,j)) + (B * (i,j))) + (C * (i,j))
by A1, A4, Def5
.=
(A * (i,j)) + ((B * (i,j)) + (C * (i,j)))
by RLVECT_1:def 3
.=
(A * (i,j)) + ((B + C) * (i,j))
by A3, A1, A4, Def5
.=
(A + (B + C)) * (
i,
j)
by A1, A4, Def5
;
verum end;
hence
(A + B) + C = A + (B + C)
by MATRIX_0:27; verum