let X be set ; :: thesis: for a, b, c being Element of (bspace X)
for A, B, C being Subset of X st a = A & b = B & c = C holds
( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C )
let a, b, c be Element of (bspace X); :: thesis: for A, B, C being Subset of X st a = A & b = B & c = C holds
( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C )
let A, B, C be Subset of X; :: thesis: ( a = A & b = B & c = C implies ( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C ) )
assume A1: ( a = A & b = B & c = C ) ; :: thesis: ( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C )
thus a + (b + c) = A \+\ (B \+\ C) :: thesis: (a + b) + c = (A \+\ B) \+\ C

proof

b + c = B \+\ C by A1, Def5;
hence a + (b + c) = A \+\ (B \+\ C) by A1, Def5; :: thesis: verum

end;

thus (a + b) + c = (A \+\ B) \+\ C :: thesis: verum

proof

a + b = A \+\ B by A1, Def5;
hence (a + b) + c = (A \+\ B) \+\ C by A1, Def5; :: thesis: verum

end;