let X be set ; :: thesis: bspace X is add-associative

let x, y, z be Element of (bspace X); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)

reconsider A = x, B = y, C = z as Subset of X ;

x + (y + z) = A \+\ (B \+\ C) by Lm1

.= (A \+\ B) \+\ C by XBOOLE_1:91

.= (x + y) + z by Lm1 ;

hence (x + y) + z = x + (y + z) ; :: thesis: verum

let x, y, z be Element of (bspace X); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)

reconsider A = x, B = y, C = z as Subset of X ;

x + (y + z) = A \+\ (B \+\ C) by Lm1

.= (A \+\ B) \+\ C by XBOOLE_1:91

.= (x + y) + z by Lm1 ;

hence (x + y) + z = x + (y + z) ; :: thesis: verum