let E be RealLinearSpace; :: thesis: for v being Element of E
for C, A being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)
let v be Element of E; :: thesis: for C, A being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)
let C, A be non empty binary-image of E; :: thesis: (erosion C) . (v + A) = v + ((erosion C) . A)
P1: (erosion C) . (v + A) = (v + A) (-) C by def030;
v + ((erosion C) . A) = v + (A (-) C) by def030;
hence (erosion C) . (v + A) = v + ((erosion C) . A) by Th120, P1; :: thesis: verum