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 ((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;

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 ((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 :: thesis: for i, j being Nat st [i,j] in Indices ((A + B) + C) holds

((A + B) + C) * (i,j) = (A + (B + C)) * (i,j)

hence
(A + B) + C = A + (B + C)
by MATRIX_0:27; :: thesis: verum((A + B) + C) * (i,j) = (A + (B + C)) * (i,j)

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 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 ;

:: thesis: verum

end;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 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 ;

:: thesis: verum