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

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