let V be RealLinearSpace; :: thesis: for p being Element of V
for a, b, c being Real holds ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)
let p be Element of V; :: thesis: for a, b, c being Real holds ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)
let a, b, c be Real; :: thesis: ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)
thus ((a + b) + c) * p = ((a + b) * p) + (c * p) by RLVECT_1:def 9
.= ((a * p) + (b * p)) + (c * p) by RLVECT_1:def 9 ; :: thesis: verum