let E be RealLinearSpace; :: thesis: for A, B, C 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 A, B, C 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 Def2
.= (A (+) B) (+) C by Def2
.= A (+) (B (+) C) by Th10
.= A (+) ((dilation C) . B) by Def2
.= (dilation ((dilation C) . B)) . A by Def2 ; :: thesis: (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A
thus (erosion C) . ((erosion B) . A) = (erosion C) . (A (-) B) by Def3
.= (A (-) B) (-) C by Def3
.= A (-) (B (+) C) by Th25
.= A (-) ((dilation C) . B) by Def2
.= (erosion ((dilation C) . B)) . A by Def3 ; :: thesis: verum