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

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