let E be RealLinearSpace; :: thesis: for A, B, C being non empty binary-image of E st A c= B holds

(dilation C) . A c= (dilation C) . B

let A, B, C be non empty binary-image of E; :: thesis: ( A c= B implies (dilation C) . A c= (dilation C) . B )

assume A1: A c= B ; :: thesis: (dilation C) . A c= (dilation C) . B

A2: (dilation C) . A = C + A by Def2;

(dilation C) . B = C + B by Def2;

hence (dilation C) . A c= (dilation C) . B by A2, A1, Th16; :: thesis: verum

(dilation C) . A c= (dilation C) . B

let A, B, C be non empty binary-image of E; :: thesis: ( A c= B implies (dilation C) . A c= (dilation C) . B )

assume A1: A c= B ; :: thesis: (dilation C) . A c= (dilation C) . B

A2: (dilation C) . A = C + A by Def2;

(dilation C) . B = C + B by Def2;

hence (dilation C) . A c= (dilation C) . B by A2, A1, Th16; :: thesis: verum