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

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