let X be set ; :: thesis: bspace X is right_zeroed
let x be Element of (bspace X); :: according to RLVECT_1:def 4 :: thesis: x + (0. (bspace X)) = x
reconsider A = x as Subset of X ;
reconsider Z = 0. (bspace X) as Subset of X ;
x + (0. (bspace X)) = A \+\ Z by Def5
.= x ;
hence x + (0. (bspace X)) = x ; :: thesis: verum