let E be RealLinearSpace; :: thesis: for C, A being non empty binary-image of E holds
( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) & (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )
let C, A be non empty binary-image of E; :: thesis: ( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) & (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )
thus (dilation C) . ( the carrier of E \ A) = ( the carrier of E \ A) (+) C by def020
.= the carrier of E \ (A (-) C) by Th106
.= the carrier of E \ ((erosion C) . A) by def030 ; :: thesis: (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A)
thus (erosion C) . ( the carrier of E \ A) = ( the carrier of E \ A) (-) C by def030
.= the carrier of E \ (A (+) C) by Th106
.= the carrier of E \ ((dilation C) . A) by def020 ; :: thesis: verum