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