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

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