let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y being Subset of T
for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p
let X, Y be Subset of T; :: thesis: for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p
let p be Point of T; :: thesis: (X + p) (o) Y = (X (o) Y) + p
thus (X + p) (o) Y = ((X (+) Y) + p) (-) Y by Th15
.= (X (o) Y) + p by Th14 ; :: thesis: verum