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