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