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