let X be set ; :: thesis: for u, v being Element of (bspace X)
for x being Element of X holds (u + v) @ x = (u @ x) + (v @ x)
let u, v be Element of (bspace X); :: thesis: for x being Element of X holds (u + v) @ x = (u @ x) + (v @ x)
let x be Element of X; :: thesis: (u + v) @ x = (u @ x) + (v @ x)
reconsider u9 = u, v9 = v as Subset of X ;
(u + v) @ x = (u9 \+\ v9) @ x by Def5
.= (u9 @ x) + (v9 @ x) by Th15 ;
hence (u + v) @ x = (u @ x) + (v @ x) ; :: thesis: verum