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 AS: A c= B ; :: thesis: (dilation C) . A c= (dilation C) . B
P1: (dilation C) . A = C + A by def020;
(dilation C) . B = C + B by def020;
hence (dilation C) . A c= (dilation C) . B by P1, AS, Th112; :: thesis: verum