let OAS be OAffinSpace; :: thesis: id the carrier of OAS is dilatation
for x, y being Element of OAS holds x,y '||' (id the carrier of OAS) . x,(id the carrier of OAS) . y by DIRAF:19;
hence id the carrier of OAS is dilatation by Th34; :: thesis: verum