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 that
A1: a = A and
A2: b = B and
A3: c = C ; :: thesis: ( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C )
b + c = B \+\ C by A2, A3, Def5;
hence a + (b + c) = A \+\ (B \+\ C) by A1, Def5; :: thesis: (a + b) + c = (A \+\ B) \+\ C
a + b = A \+\ B by A1, A2, Def5;
hence (a + b) + c = (A \+\ B) \+\ C by A3, Def5; :: thesis: verum