let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: (A + B) + C = A + (B + C)
A1: ( Indices A = Indices B & Indices A = Indices C ) by Th27;
A2: ( Indices A = Indices ((A + B) + C) & Indices A = Indices (A + (B + C)) ) by Th27;
A3: ( Indices A = Indices (A + B) & Indices A = Indices (B + C) ) by Th27;

now

let i, j be Nat; :: thesis: ( [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) ; :: thesis: ((A + B) + C) * i,j = (A + (B + C)) * i,j
hence ((A + B) + C) * i,j = ((A + B) * i,j) + (C * i,j) by A2, A3, Def14
.= ((A * i,j) + (B * i,j)) + (C * i,j) by A2, A4, Def14
.= (A * i,j) + ((B * i,j) + (C * i,j)) by RLVECT_1:def 6
.= (A * i,j) + ((B + C) * i,j) by A1, A2, A4, Def14
.= (A + (B + C)) * i,j by A2, A4, Def14 ;
:: thesis: verum

end;

hence (A + B) + C = A + (B + C) by Th28; :: thesis: verum