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